Transcript necula

The Future of
Correct Software
George Necula
Software Correctness is Important
► Where
there is software, there are bugs
► It
is estimated that software bugs cost the
economy over $60B a year (1% of GDP)
 Average cost of downtime can be $1M/hour
► Software
bugs are responsible for over 50%
of known security vulnerabilities
2
Software Correctness is Hard
► Social
challenges
 Customers still favor features and performance
 Programmers notoriously overconfident
► Economic
challenges
 Correctness costs more than extra features
► Technical
challenges
 Impossible to build perfect software quality tools
 False alarms and missed errors are facts of life
3
The Open Source Quality Group
► Members
 Rastislav Bodik, George Necula, Sanjit Seshia
 Collaborators at Stanford, Microsoft, IBM, Intel
 And 15 graduate students
►
Develop techniques and tools for building,
deploying and monitoring quality software
► Use
Open Source software as a test bed
4
1. Building Correct Software
► Tools
can help only if we bring more
information in the software process
► Find unobtrusive ways to get programmer
assistance with correctness reasoning
 Programs express “how” things must be done
 Programmers know the “what” and “why” !
► Example:
Programming by sketching
 by Rastislav Bodik, Sanjit Seshia
5
The Sketching Experience
spec
+
specification
sketch
implementation
(completed sketch)
6
Promising Properties
Sketched programs are developed …
rapidly: the low-level details are synthesized
automatically
correctly: implementation guaranteed to behave
like the specification
7
Example: Sorting by hand
int[] merge (int[] a, int b[], int n) {
for (int i = 0; i < n; i++)
if ( j<n && ( !(k<n) || a[j] < b[k]) ) {
result[i] = a[j]; j++;
} else {
result[i] = b[k]; k++;
}
}
return result;
}
► The
devil is in the details
8
Sorting sketched
int[] merge (int[] a, int b[], int n) {
for (int i = 0; i < n; i++)
if ( synthesize(
||, &&, <, !, [] ) ) {
hole
result[i] = a[j]; j++;
} else {
result[i] = b[k]; k++;
}
}
return result;
}
►
►
►
Sketch compiler fills in the details correctly
Sketches are programs with missing details
Specifications can be slow/simple programs
9
Experience with Sketching Ciphers
User experiment:
 goal: implement a mini-cipher
 how: C programmer vs. sketching programmer
Results:
 sketching programmer was twice as fast
 sketched cipher ran 50% faster
Next: sketching for general purpose programs
10
2. Deploying Correct Software
► Today’s
view of software:
 Software is executable
► Future
view of software:
 Software is checkable and executable
► We
need to redefine what software is:
Software =
Executable content
+ Assurance support
11
Today: Digital Signatures
Code
Signature
Trust the code producer
Signature
Checking
• Not a behavioral assurance
• Dangerous !
• Does not scale well
Good but not enough
CPU
Consumer
12
Future: Semantic Assurance
Code
Safety Proof
Code producer “helps” the
consumer to check the code
Proof
Checking
• Proof-carrying code
• Provides semantic assurance
• Producer does the hard work
CPU
Consumer
13
Challenges
► How
small can you make the proofs?
 Today about 25% of the code and shrinking
► How
do you generate proofs ?
 Certifying software synthesis tools (compilers)
 Automatic today for memory safety, resource
usage constraints
► Next:
make more software tools certifying
14
3. When Everything Else Fails
►
►
The future of correct software must include
incorrect software
We must deal with execution errors
 Monitoring, recovery, restarting, …
►
Example: Cooperative Bug Isolation
15
Post-Deployment Monitoring
Cooperative Bug Isolation
16
Idea: Measure Reality
► Go
beyond measuring crashes
► Monitor good and bad executions
 Spread cost of monitoring over many users
 Collect feedback data & mine for bug causes
► Actual
user runs are a vast resource
 Number of real runs >> number of testing runs
 Real-world executions are most important
17
Bug Isolation Architecture
Sampler
Program
Source
Top bugs with
likely causes
Compiler
Statistical
Debugging
Shipping
Application
Pro le
J/L
18
Public Deployment in Progress
10%
8%
6%
success runs
failure runs
4%
2%
►
►
SP
IM
bo
x
th
m
s
Rh
y
til
u
Na
u
c
G
nu
m
er
i
P
IM
Th
eG
ai
m
G
Ev
ol
ut
io
n
0%
Applications do have bugs
Attract more users for statistical analysis
19
Conclusion
►
Social factors will work in favor of software
correctness
►
Technology must provide affordable
solutions for correctness
 Bring more information into software process
 Software synthesis from high-level specifications
 Software distributions with assurance support
►
Good error handling always important
20