Flow logic for language-based safety and security

Society is increasingly dependent on information and communication technology. Computers are integrated into everything from toasters to control systems for critical infrastructure. Consequently even simple programming errors have the potential to wreck havoc on practically every aspect of society and everyday life.

It is therefore a crucial challenge for computer science to develop tools and techniques that can help improve the quality of software design and implementation. In this dissertation it is argued that techniques rooted in the theory and practice of programming languages, so-called language-based safety and security, provide a feasible platform for developing software that can be verified and validated with a very high degree of assurance.

Specifically, it is argued and demonstrated that static analysis is an indispensable technique for languagebased safety and security and that the Flow Logic framework for static analysis is particularly useful this regard. In order to support and illustrate the above points, a number of program analyses are developed for the Carmel programming language, a variant of the low-level language used on Java smart cards.

The analyses are formally proved correct with respect to the semantics and are then used to verify a wide spectrum of pertinent safety and security properties.