|Técnicas formales para la seguridad del código móvil|
Dictado por: Gilles Barthe
El curso se dictará en castellano.
The objective of the lectures is to present type-based and logic-based mechanisms to ensure reliability and security of mobile code.
The first part of the lectures shall be devoted to introductory material on mobile code security and to a general presentation of the EU project Mobius.
The second 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. I shall also survey existing work in type systems for low-level languages and Proof Carrying Code.
The third 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 show that non-optimizing compilers preserve proof obligations, and discuss approaches to stretch the results to optimizing
|< Anterior||Siguiente >|