Machine-checked software security analyses
The Idea
Software security analyses are nowadays of ever growing importance. But: Quis Custodiet Ipsos Custodes? (Who will guard the guards?). More and more such analyses are being published, many of them without any proof of correctness, others are happy with using pen-and-paper.
This project is a cooperation of two groups (Universität Karlsruhe and TU München) to construct machine checked correctness proofs for several new precise techniques in the area of Language Based Security focusing on their semantical aspects resp. falsify published techniques.
The Goals
What we want to achieve with this project:
- reaching a new level of reliability of Language Based Security
- developing new techniques to validate the underlying language description
- integrating semantics, theorem provers and program analysis with Language Based Security
The Basis
A starting point of this project are these semantics for Java and C++, both proved typesafe in Isabelle/HOL, as well as dependency analysis techniques and Information Flow Control for Java and C.
Language Based Security (LBS) uses techniques such as semantics of programming languages and program analysis. LBS examines source or object codes to guarantee certain security properties or to find security holes. A branch of LBS is the Information Flow Control (IFC) which is used to guarantee confidentiality and integrity of data.
The Tasks
In our group we focus on the following tasks:
- formalising selected LBS techniques and verifying against an operational semantics of the underlying language (Java or C++) , using theorem provers
- expanding the underlying operational semantics of Java and C++ kernels to cope with realistic programs with a special focus on concurrency
The Results
We can already present some results in expanding the underlying semantics and
formalising the basic program analysis:
- the Jinja language now incorporates arrays and threads, we adapted the
source code, byte code and compiler;
- Java2Jinja, a converter from Java to Jinja, which is available for download here
- dynamic and static intraprocedural slicing is proven correct using
a framework that abstracts from the underlying semantics;
- static context-sensitive slicing (namely, the slicing Algorithm of Horwitz, Reps, and Binkley [TOPLAS '90]) is proven correct in an extended modular framework;
- we instantiated both frameworks with the Jinja byte code semantics, thus dynamic and static intraprocedural slicing for Jinja byte code is proven correct;
- as a first result concerning Information Flow Control, we showed that slicing-based IFC guarantees Low-Deterministic Security.
An overview of the results can be found in these slides.
Funded by the DFG. Previous work was done at the University of Passau.
Participants
Publications
|
