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. Testing is |
10 we need a more principled approach to programming. Testing is |
11 good, but as Dijkstra famously said ``Testing can only show |
11 good, but as Dijkstra famously said: ``Testing can only show |
12 the presence of bugs, not their absence''. While such a more |
12 the presence of bugs, not their absence''. While such a more |
13 principled approach has been the subject of intense study for |
13 principled approach has been the subject of intense study for |
14 a long time, only in the past recent years some impressive |
14 a long time, only in the past few years some impressive |
15 results have been achieved. One is the complete formalisation |
15 results have been achieved. One is the complete formalisation |
16 and (mathematical) verification of a microkernel operating |
16 and (mathematical) verification of a microkernel operating |
17 system called seL4. |
17 system called seL4. |
18 |
18 |
19 \begin{center} |
19 \begin{center} |
20 \url{http://sel4.systems} |
20 \url{http://sel4.systems} |
21 \end{center} |
21 \end{center} |
22 |
22 |
23 \noindent In 2011 this work was included in the MIT Technology |
23 \noindent In 2011, this work was included in the MIT |
24 Review in the annual list of the world’s ten most important |
24 Technology Review in the annual list of the world’s ten most |
25 emerging |
25 important emerging |
26 technologies.\footnote{\url{http://www2.technologyreview.com/tr10/?year=2011}} |
26 technologies.\footnote{\url{http://www2.technologyreview.com/tr10/?year=2011}} |
27 While this work is impressive, it technical details are too |
27 While this work is impressive, its technical details are too |
28 numerous that they can be explained here. So let us look at |
28 enormous for explanation here. Therefore let us look at |
29 something much simpler, namely finding out properties about |
29 something much simpler, namely finding out properties about |
30 programs in a very simple programming language using |
30 programs using \emph{static analysis}. |
31 \emph{static analysis}. |
|
32 |
31 |
|
32 Static analysis is one technique that checks properties |
|
33 of a program without actually running the program. This |
|
34 should raise alarm bells---the reason that almost all |
|
35 interesting properties about programs are equivalent to |
|
36 the halting problem, which we know is undecidable. |
|
37 |
|
38 \bigskip |
33 |
39 |
34 \noindent What would be missing in comparison with real |
40 \noindent What would be missing in comparison with real |
35 (low-level machine) code? Well, the numbers we assume to be |
41 (low-level machine) code? Well, the numbers we assume to be |
36 arbitrary precision, which is not the case in real code. There |
42 arbitrary precision, which is not the case in real code. There |
37 basic number formats have a rang and might over-run or |
43 basic number formats have a rang and might over-run or |