Treffer: Verification Methods for Software Security and Correctness

The objective of the lectures is to present type-based and logic-based mechanisms to ensure reliability and security of mobile code. In the first part of the lectures, I shall present two enforcement mechanisms for low-level code. The first mechanism is a verifier for ensuring information flow policies for confidentiality: it is a type-base mechanism, compatible with the principles of Java lightweight bytecode verification. The second mechanism is a verification condition generator for programs specified with logical annotations (pre-conditions, post-conditions, etc). It is a logic-based mechanism that permits to verify complex security policies as well as functional correctness, and is used in the context of Proof Carrying Code. Due to their complexity and to their important role in the Trusted Computing Base, it is central that these mechanisms are shown correct with the highest confidence; I shall also describe how these mechanisms have been certified using the proof assistant Coq. In the second part of the lectures, I shall relate these two enforcement mechanisms to their counterparts for source code programs. In the case of information flow typing, I shall show that non-optimizing compilers preserve typing, i.e. transform source programs typable with an information flow system into target programs that are accepted by an information flow bytecode verifier. In the case of functional correctness, I shall