Proof Automation
Class 2: Ethics
Lightning Lecture
2
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an OS kernel. SOSP 2009.
Last Class
✓
“Of course we want to make
autonomous helicopters safe!”
- naive me
3
“Of course we want to make
autonomous helicopters safe!”
- naive me
4
“Of course we want to make
military drones safe!”
- naive me
5
“Of course we want to make
military drones safe!”
- naive me
6
?
?
?
?
?
“Of course we want to make
military drones safe!”
- naive me
7
?
?
?
?
?
Who benefits?
“Of course we want to make
military drones safe!”
- naive me
8
?
?
?
?
?
Who benefits?
Is hacking justified?
“Of course we want to make
military drones safe!”
- naive me
9
?
?
?
?
?
Who benefits?
Is hacking justified?
Is participation inherently bad?
“Of course we want to make
military drones safe!”
- naive me
10
?
?
?
?
?
Who benefits?
Is hacking justified?
Is participation inherently bad?
Who is responsible?
“Of course we want to make
military drones safe!”
- naive me
11
?
?
?
?
?
Who benefits?
Is hacking justified?
Is participation inherently bad?
Who is responsible?
Does the good outweigh the bad?
“Verification is inherently good.”
- naive me
12
Is it good to verify a drone?
- naive me
13
Verification is a technology that can be used for profound good
and for profound evil.
- naive me
14
Proof automation makes it
easier to do profound good
and profound evil.
- naive me
15
Dual Use:
when your research makes it
easier to do profound good
and profound evil.
- naive me
16
Dual Use:
when your research makes it
easier to do profound good
and profound evil. This is everywhere in PL/FM/SE.
17
Ethics in Proof Automation
18
Ethics has more questions
than answers.
19
?
?
?
?
?
Ethics in Proof Automation
There isn’t a single universal
ethical framework.
20
Ethics in Proof Automation
The ACM Ethics Code is one
ethical framework.
21
Ethics in Proof Automation
The ACM Ethics Code is one
ethical framework. Most of you are bound by it.
22
Ethics in Proof Automation
23
A computing professional should...
1.1 Contribute to society and to human well-being,
acknowledging that all people are stakeholders in computing.
1.2 Avoid harm.
1.3 Be honest and trustworthy.
1.4 Be fair and take action not to discriminate.
1.5 Respect the work required to produce new ideas, inventions,
creative works, and computing artifacts.
1.6 Respect privacy.
1.7 Honor confidentiality.
24
ACM Ethics Code
General Ethical Principles
A computing professional should...
1.1 Contribute to society and to human well-being,
acknowledging that all people are stakeholders in computing.
1.2 Avoid harm.
1.3 Be honest and trustworthy.
1.4 Be fair and take action not to discriminate.
1.5 Respect the work required to produce new ideas, inventions,
creative works, and computing artifacts.
1.6 Respect privacy.
1.7 Honor confidentiality.
25
ACM Ethics Code
General Ethical Principles
A computing professional should...
1.1 Contribute to society and to human well-being,
acknowledging that all people are stakeholders in computing.
1.2 Avoid harm.
1.3 Be honest and trustworthy.
1.4 Be fair and take action not to discriminate.
1.5 Respect the work required to produce new ideas, inventions,
creative works, and computing artifacts.
1.6 Respect privacy.
1.7 Honor confidentiality.
26
ACM Ethics Code
General Ethical Principles
?
?
A computing professional should...
1.1 Contribute to society and to human well-being,
acknowledging that all people are stakeholders in computing.
1.2 Avoid harm.
1.3 Be honest and trustworthy.
1.4 Be fair and take action not to discriminate.
1.5 Respect the work required to produce new ideas, inventions,
creative works, and computing artifacts.
1.6 Respect privacy.
1.7 Honor confidentiality.
27
ACM Ethics Code
General Ethical Principles
A computing professional should...
1.1 Contribute to society and to human well-being,
acknowledging that all people are stakeholders in computing.
1.2 Avoid harm.
1.3 Be honest and trustworthy.
1.4 Be fair and take action not to discriminate.
1.5 Respect the work required to produce new ideas, inventions,
creative works, and computing artifacts.
1.6 Respect privacy.
1.7 Honor confidentiality.
28
ACM Ethics Code
General Ethical Principles
A computing professional should...
1.1 Contribute to society and to human well-being,
acknowledging that all people are stakeholders in computing.
1.2 Avoid harm.
1.3 Be honest and trustworthy.
1.4 Be fair and take action not to discriminate.
1.5 Respect the work required to produce new ideas, inventions,
creative works, and computing artifacts.
1.6 Respect privacy.
1.7 Honor confidentiality.
29
ACM Ethics Code
General Ethical Principles
?
A computing professional should...
1.1 Contribute to society and to human well-being,
acknowledging that all people are stakeholders in computing.
1.2 Avoid harm.
1.3 Be honest and trustworthy.
1.4 Be fair and take action not to discriminate.
1.5 Respect the work required to produce new ideas, inventions,
creative works, and computing artifacts.
1.6 Respect privacy.
1.7 Honor confidentiality.
30
ACM Ethics Code
General Ethical Principles
?
?
A computing professional should...
1.1 Contribute to society and to human well-being,
acknowledging that all people are stakeholders in computing.
1.2 Avoid harm.
1.3 Be honest and trustworthy.
1.4 Be fair and take action not to discriminate.
1.5 Respect the work required to produce new ideas, inventions,
creative works, and computing artifacts.
1.6 Respect privacy.
1.7 Honor confidentiality.
31
ACM Ethics Code
General Ethical Principles
?
?
?
A computing professional should...
1.1 Contribute to society and to human well-being,
acknowledging that all people are stakeholders in computing.
1.2 Avoid harm.
1.3 Be honest and trustworthy.
1.4 Be fair and take action not to discriminate.
1.5 Respect the work required to produce new ideas, inventions,
creative works, and computing artifacts.
1.6 Respect privacy.
1.7 Honor confidentiality.
32
ACM Ethics Code
General Ethical Principles
?
?
?
?
A computing professional should...
1.1 Contribute to society and to human well-being,
acknowledging that all people are stakeholders in computing.
1.2 Avoid harm.
1.3 Be honest and trustworthy.
1.4 Be fair and take action not to discriminate.
1.5 Respect the work required to produce new ideas, inventions,
creative works, and computing artifacts.
1.6 Respect privacy.
1.7 Honor confidentiality.
33
ACM Ethics Code
General Ethical Principles
?
?
?
✓
A computing professional should...
2.1 Strive to achieve high quality in … professional work.
2.2 Maintain high standards of … competence … and ethical practice.
2.3 Know and respect existing rules pertaining to professional work.
2.4 Accept and provide appropriate professional review.
2.5 Give comprehensive and thorough evaluations of … systems …
2.6 Perform work only in areas of competence.
2.7 Foster public awareness … of computing … and … consequences.
2.8 Access computing and communication resources only when
authorized or when compelled by the public good.
2.9 Design and implement systems that are robustly and
usably secure.
34
ACM Ethics Code
Professional Responsibilities
✓
✓
A computing professional should...
2.1 Strive to achieve high quality in … professional work.
2.2 Maintain high standards of … competence … and ethical practice.
2.3 Know and respect existing rules pertaining to professional work.
2.4 Accept and provide appropriate professional review.
2.5 Give comprehensive and thorough evaluations of … systems …
2.6 Perform work only in areas of competence.
2.7 Foster public awareness … of computing … and … consequences.
2.8 Access computing and communication resources only when
authorized or when compelled by the public good.
2.9 Design and implement systems that are robustly and
usably secure.
35
ACM Ethics Code
Professional Responsibilities
✓
✓
✓
A computing professional should...
2.1 Strive to achieve high quality in … professional work.
2.2 Maintain high standards of … competence … and ethical practice.
2.3 Know and respect existing rules pertaining to professional work.
2.4 Accept and provide appropriate professional review.
2.5 Give comprehensive and thorough evaluations of … systems …
2.6 Perform work only in areas of competence.
2.7 Foster public awareness … of computing … and … consequences.
2.8 Access computing and communication resources only when
authorized or when compelled by the public good.
2.9 Design and implement systems that are robustly and
usably secure.
36
ACM Ethics Code
Professional Responsibilities
✓
✓
✓
?
A computing professional should...
2.1 Strive to achieve high quality in … professional work.
2.2 Maintain high standards of … competence … and ethical practice.
2.3 Know and respect existing rules pertaining to professional work.
2.4 Accept and provide appropriate professional review.
2.5 Give comprehensive and thorough evaluations of … systems …
2.6 Perform work only in areas of competence.
2.7 Foster public awareness … of computing … and … consequences.
2.8 Access computing and communication resources only when
authorized or when compelled by the public good.
2.9 Design and implement systems that are robustly and
usably secure.
37
ACM Ethics Code
Professional Responsibilities
A computing professional should...
2.1 Strive to achieve high quality in … professional work.
2.2 Maintain high standards of … competence … and ethical practice.
2.3 Know and respect existing rules pertaining to professional work.
… Computing professionals must abide by … rules unless there is a
compelling ethical justification to do otherwise. Rules that are
judged unethical should be challenged … A computing professional
should consider challenging the rule through existing channels
before violating the rule. A computing professional who decides to
violate a rule because it is unethical, or for any other reason, must
consider potential consequences and accept responsibility …
38
ACM Ethics Code
Professional Responsibilities
A computing professional should...
2.1 Strive to achieve high quality in … professional work.
2.2 Maintain high standards of … competence … and ethical practice.
2.3 Know and respect existing rules pertaining to professional work.
… Computing professionals must abide by … rules unless there is a
compelling ethical justification to do otherwise. Rules that are
judged unethical should be challenged … A computing professional
should consider challenging the rule through existing channels
before violating the rule. A computing professional who decides to
violate a rule because it is unethical, or for any other reason, must
consider potential consequences and accept responsibility …
39
ACM Ethics Code
Professional Responsibilities
A computing professional should...
2.1 Strive to achieve high quality in … professional work.
2.2 Maintain high standards of … competence … and ethical practice.
2.3 Know and respect existing rules pertaining to professional work.
… Computing professionals must abide by … rules unless there is a
compelling ethical justification to do otherwise. Rules that are
judged unethical should be challenged … A computing professional
should consider challenging the rule through existing channels
before violating the rule. A computing professional who decides to
violate a rule because it is unethical, or for any other reason, must
consider potential consequences and accept responsibility …
40
ACM Ethics Code
Professional Responsibilities
A computing professional should...
2.1 Strive to achieve high quality in … professional work.
2.2 Maintain high standards of … competence … and ethical practice.
2.3 Know and respect existing rules pertaining to professional work.
… Computing professionals must abide by … rules unless there is a
compelling ethical justification to do otherwise. Rules that are
judged unethical should be challenged … A computing professional
should consider challenging the rule through existing channels
before violating the rule. A computing professional who decides to
violate a rule because it is unethical, or for any other reason, must
consider potential consequences and accept responsibility …
41
ACM Ethics Code
Professional Responsibilities
A computing professional should...
2.1 Strive to achieve high quality in … professional work.
2.2 Maintain high standards of … competence … and ethical practice.
2.3 Know and respect existing rules pertaining to professional work.
… Computing professionals must abide by … rules unless there is a
compelling ethical justification to do otherwise. Rules that are
judged unethical should be challenged … A computing professional
should consider challenging the rule through existing channels
before violating the rule. A computing professional who decides to
violate a rule because it is unethical, or for any other reason, must
consider potential consequences and accept responsibility …
42
ACM Ethics Code
Professional Responsibilities
A computing professional should...
2.1 Strive to achieve high quality in … professional work.
2.2 Maintain high standards of … competence … and ethical practice.
2.3 Know and respect existing rules pertaining to professional work.
… Computing professionals must abide by … rules unless there is a
compelling ethical justification to do otherwise. Rules that are
judged unethical should be challenged … A computing professional
should consider challenging the rule through existing channels
before violating the rule. A computing professional who decides to
violate a rule because it is unethical, or for any other reason, must
consider potential consequences and accept responsibility …
43
ACM Ethics Code
Professional Responsibilities
?
44
ACM Ethics Code
An Aside on Sponsors
45
ACM Ethics Code
An Aside on Sponsors
$$$
$$$
46
ACM Ethics Code
An Aside on Sponsors
$$$$$$$$$
$$$
47
ACM Ethics Code
An Aside on Sponsors
$$$$$$$$$
$$$
$$$$$$$$$
48
ACM Ethics Code
An Aside on Sponsors
$$$$$$$$$
$$$
$$$$$$$$$
?
?
?
49
ACM Ethics Code
An Aside on Sponsors
$$$
50
ACM Ethics Code
An Aside on Sponsors
$$$
51
ACM Ethics Code
An Aside on Sponsors
$$$
?
?
52
ACM Ethics Code
An Aside on Sponsors
$$$
A computing professional, especially one acting as a leader, should...
3.1 Ensure that the public good is the central concern during all
professional computing work.
3.2 Articulate, encourage acceptance of, and evaluate fulfillment of
social responsibilities by members of the organization or group.
3.3 Manage … resources to enhance the quality of working life.
3.4 Articulate, apply, and support policies and processes that
reflect the principles of the Code.
3.5 Create opportunities … to grow as professionals.
3.6 Use care when modifying or retiring systems.
3.7 Recognize and take special care of systems that become
integrated into the infrastructure of society.
53
ACM Ethics Code
Professional Leadership Principles
A computing professional, especially one acting as a leader, should...
3.1 Ensure that the public good is the central concern during all
professional computing work.
3.2 Articulate, encourage acceptance of, and evaluate fulfillment of
social responsibilities by members of the organization or group.
3.3 Manage … resources to enhance the quality of working life.
3.4 Articulate, apply, and support policies and processes that
reflect the principles of the Code.
3.5 Create opportunities … to grow as professionals.
3.6 Use care when modifying or retiring systems.
3.7 Recognize and take special care of systems that become
integrated into the infrastructure of society.
54
ACM Ethics Code
Professional Leadership Principles
What You Can Do
55
56
What You Can Do
Direct Confrontation
57
What You Can Do
Direct Confrontation
58
What You Can Do
$$$$$$$$$
Direct Confrontation
59
What You Can Do
$$$$$$$$$
Direct Confrontation
60
What You Can Do
Direct Confrontation
61
What You Can Do
Not always safe!
Ask a Mentor
62
What You Can Do
Ask a Friend
63
What You Can Do
Get Into Department Policy
64
What You Can Do
Get Into SIGPLAN Policy
65
What You Can Do
Get Into ACM Policy
66
What You Can Do
Get Into National Tech Policy
67
What You Can Do
Case Studies
68
Next Class
69
70
Next Class
Post!
71
Sign Up!
Next Class
Philosophy of Logic
Ethics
Dependent Type Theory
Language Design
Solver-Aided Verification
Program Synthesis
Compilers
Systems
Security
Software Engineering
Human-Computer Interaction
Deep Learning
72
Foundations
Next Class
I hope you feel
informed and empowered
to ask questions
and do the right thing.
73