1 Department of Informatics and Mathematical Modeling, Technical University of Denmark2 Language-Based Technology, Department of Informatics and Mathematical Modeling, Technical University of Denmark3 Department of Applied Mathematics and Computer Science, Technical University of Denmark
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 language- based 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.