sen-material: handouts/ho09.tex@f1491e0d7be0 (annotated)

276 d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1	\documentclass{article}
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2	\usepackage{../style}
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	\usepackage{../langs}
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	\begin{document}
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6
335 06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	7	\section*{Handout 9 (Static Analysis)}
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	8
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	9	If we want to improve the safety and security of our programs,
337 92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	10	we need a more principled approach to programming. Testing is
338 f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	11	good, but as Dijkstra famously said: ``Testing can only show
337 92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	12	the presence of bugs, not their absence''. While such a more
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	13	principled approach has been the subject of intense study for
338 f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	14	a long time, only in the past few years some impressive
337 92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	15	results have been achieved. One is the complete formalisation
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	16	and (mathematical) verification of a microkernel operating
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	17	system called seL4.
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	18
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	19	\begin{center}
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	20	\url{http://sel4.systems}
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	21	\end{center}
92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	22
338 f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	23	\noindent In 2011, this work was included in the MIT
f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	24	Technology Review in the annual list of the world’s ten most
f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	25	important emerging
337 92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	26	technologies.\footnote{\url{http://www2.technologyreview.com/tr10/?year=2011}}
338 f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	27	While this work is impressive, its technical details are too
f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	28	enormous for explanation here. Therefore let us look at
337 92a718b88e14 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 335 diff changeset	29	something much simpler, namely finding out properties about
338 f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	30	programs using \emph{static analysis}.
335 06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	31
338 f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	32	Static analysis is one technique that checks properties
f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	33	of a program without actually running the program. This
f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	34	should raise alarm bells---the reason that almost all
f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	35	interesting properties about programs are equivalent to
f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	36	the halting problem, which we know is undecidable.
f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	37
f1491e0d7be0 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 337 diff changeset	38	\bigskip
276 d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39
335 06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	40	\noindent What would be missing in comparison with real
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	41	(low-level machine) code? Well, the numbers we assume to be
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	42	arbitrary precision, which is not the case in real code. There
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	43	basic number formats have a rang and might over-run or
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	44	under-run from this range. Our assumption about variables,
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	45	does not correspond to actual registers, which are only
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	46	limited on real hardware. Obviously, real code has richer
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	47	operations than just addition, multiplication and equality.
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	48	But this are not really essential limitations of our simple
06d5fc15594d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 276 diff changeset	49	examples.
276 d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51	\end{document}
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	53	%%% Local Variables:
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54	%%% mode: latex
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55	%%% TeX-master: t
d7109c6e721d updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Mon, 01 Dec 2014 06:50:25 +0000
changeset 338	f1491e0d7be0
parent 337	92a718b88e14
child 346	5a6e8b7d20f7
permissions	-rw-r--r--