HOME | ENGLISH | IMPRESSUM | KIT

Quis-Custodiet

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 constructs 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, in particular 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
  • formal and machine-checked treatment of semantics for lazy fuctional programming languages and their application to program analyses

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.
  • in the realm of functional programming laguages, we implemented various semantics in Isabelle and used them to proof a program analysis performed by the GHC Haskell compiler to be correctness

An overview of the results can be found in these slides.

Funded by the DFG. Previous work was done at the University of Passau. Part of the project was done in cooperation with TU München.

Projektbeteiligte

Lehrstuhlinhaber
Prof. Gregor Snelting
Wissenschaftliche Mitarbeiter
Denis Lohner
Ehemalige Mitarbeiter
Dr. rer. nat. Joachim Breitner
Dr. rer. nat. Andreas Lochbihler
Dr.-Ing. Daniel Wasserrab

Veröffentlichungen

2017
M. Wagner, D. Lohner: Minimal Static Single Assignment Form. AFP 2017
2016
S. Ullrich, D. Lohner: Verified Construction of Static Single Assignment Form. AFP 2016
S. Buchwald, D. Lohner, S. Ullrich: Verified Construction of Static Single Assignment Form. CC 2016
2015
J. Breitner: The Safety of Call Arity. AFP 2015
2014
G. Snelting, D. Giffhorn, J. Graf, C. Hammer, M. Hecker, M. Mohr, D. Wasserrab: Checking Probabilistic Noninterference Using JOANA. IT 2014
A. Lochbihler: Making the Java Memory Model Safe. TOPLAS 2014
2013
A. Lochbihler: Light-weight Containers. AFP 2013
J. Breitner: The Correctness of Launchbury's Natural Semantics for Lazy Evaluation. AFP 2013
A. Lochbihler: Ein maschinengeprüftes, typsicheres Modell der Nebenläufigkeit in Java: Sprachdefinition, virtuelle Maschine, Speichermodell und verifizierter Compiler. LNI - Ausgezeichnete Informatikdissertationen 2012
A. Lochbihler: Light-weight containers for Isabelle: efficient, extensible, nestable. ITP 2013
2012
A. Lochbihler: The Java Memory Model is Type Safe.
K. Kohlmeyer: Funktionale Konstruktion und Verifikation von Kontrollflussgraphen.
A. Lochbihler: A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler.
A. Lochbihler: Java and the Java Memory Model -- a Unified, Machine-Checked Formalisation. ESOP 2012
2011
A. Lochbihler: A Unified, Machine-Checked Formalisation of Java and the Java Memory Model.
A. Lochbihler, L. Bulwahn: Animating the Formalised Semantics of a Java-like Language. ITP 2011
2010
J. Breitner: Shivers' Control Flow Analysis. AFP 2010
J. Breitner: Control Flow in Functional Languages -- Formally taming lambdas.
J. Breitner: The shivers-cfg package. Haskell library
D. Wasserrab: From Formal Semantics to Verified Slicing - A Modular Framework with Applications in Language Based Security. Ph.D. thesis
P. Lammich, A. Lochbihler: The Isabelle Collections Framework. ITP 2010
D. Wasserrab: Information Flow Noninterference via Slicing. AFP 2010
A. Lochbihler: Verifying a Compiler for Java Threads. ESOP 2010
J. Thedering: Entwicklung eines Übersetzers von Java nach Jinja.
A. Lochbihler: Coinductive. AFP 2010
D. Wasserrab, D. Lohner: Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing. VERIFY 2010
2009
D. Wasserrab: Backing up Slicing: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer. AFP 2009
A. Lochbihler: Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. TPHOLs 2009
D. Wasserrab, D. Lohner, G. Snelting: On PDG-Based Noninterference and its Modular Proof. PLAS 2009
A. Lochbihler: Code Generation for Functions as Data. AFP 2009
2008
G. Snelting, D. Wasserrab: A Correctness Proof for the Volpano/Smith Security Typing System. AFP 2008
D. Wasserrab: Towards Certified Slicing. AFP 2008
D. Wasserrab, A. Lochbihler: Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. TPHOLS 2008
A. Lochbihler: Type Safe Nondeterminism - A Formal Semantics of Java Threads. FOOL 2008