5 \begin{document} |
5 \begin{document} |
6 |
6 |
7 \section*{Handout 9 (Static Analysis)} |
7 \section*{Handout 9 (Static Analysis)} |
8 |
8 |
9 If we want to improve the safety and security of our programs, |
9 If we want to improve the safety and security of our programs, |
10 we need a more principled approach to programming. |
10 we need a more principled approach to programming. Testing is |
|
11 good, but as Dijkstra famously said ``Testing can only show |
|
12 the presence of bugs, not their absence''. While such a more |
|
13 principled approach has been the subject of intense study for |
|
14 a long time, only in the past recent years some impressive |
|
15 results have been achieved. One is the complete formalisation |
|
16 and (mathematical) verification of a microkernel operating |
|
17 system called seL4. |
|
18 |
|
19 \begin{center} |
|
20 \url{http://sel4.systems} |
|
21 \end{center} |
|
22 |
|
23 \noindent In 2011 this work was included in the MIT Technology |
|
24 Review in the annual list of the world’s ten most important |
|
25 emerging |
|
26 technologies.\footnote{\url{http://www2.technologyreview.com/tr10/?year=2011}} |
|
27 While this work is impressive, it technical details are too |
|
28 numerous that they can be explained here. So let us look at |
|
29 something much simpler, namely finding out properties about |
|
30 programs in a very simple programming language using |
|
31 \emph{static analysis}. |
11 |
32 |
12 |
33 |
13 \noindent What would be missing in comparison with real |
34 \noindent What would be missing in comparison with real |
14 (low-level machine) code? Well, the numbers we assume to be |
35 (low-level machine) code? Well, the numbers we assume to be |
15 arbitrary precision, which is not the case in real code. There |
36 arbitrary precision, which is not the case in real code. There |