It has to be ensured that security properties are actually satisfied by the implementation after model-based elicitation of security requirements. KASTEL hence developed a concept for proving security properties in the implementation according to the requirements specified in the model. We also develop the tools necessary to perform the verification on the implementation.
Proving Security for Java programs
KASTEL develops methods for the translation of security properties in design models into specifications for Java programs. Implementations can be proven to be consistent with these specifications by using the tools KeY and JOANA.
KeY is a deductive verification tool that allows partly automated security proofs for Java source code. JOANA analyses Java byte code for information-flow properties using program dependency graphs.
To ensure that during system development the specification of a system does not drift away from its implementation, KASTEL researches approaches to keep specification and implementation consistent. We investigate approaches that allow, upon architectural relevant changes in the code, to automatically evolve the model with the implementation.
- View-centric engineering with synchronized heterogeneous models Proceedings of the 1st Workshop on View-Based, Aspect-Oriented and Orthographic Software Modelling
Specification and Proof for Complex Confidentiality Properties
Often complex information flow specifications for systems are necessary in order to proof the system's security. Therefore KASTEL extends the existing verification tool KeY in a way that allows tool-supported proofs for these kinds of complex requirements.
With these extensions, it was possible to formalize and proof secure information flow for the data storage of a smart surveillance system. The analyzed case shows the so called Tracking Paradox, where it is necessary to collect sensible data in order to protect it. Also, the level of security of the data stored in the system changes over time.
Further, KASTEL researches on quantitative measurement of information flow. These tools allow to formalize the amount of information that can be retrieved by reading certain data.
- Information Flow in Object-Oriented Software LOPSTR 2013: 23rd International Symposium on Logic-Based Program Synthesis and Transformation
- Privacy Preserving Surveillance and the Tracking-Paradox Future Security -- Security Research Conference 2013 (Future Security 2013)
- Precise Quantitative Information Flow Analysis -- A Symbolic Approach Theoretical Computer Science, Volume 538 (2014)
Security Proofs for Implementations of Cryptographic Protocols
Practically used systems often use encryption mechanisms in order to ensure confidentiality of information. Implementations making use of encryption can not directly be proven secure with the tools described earlier, as there does exist a flow of information from confidential data to its encryption, although it can not be retrieved with a reasonable effort.
Nevertheless, we can use cryptographic assumptions which allow us to use KeY and JOANA for proving security properties. In KASTEL, we were able to show this for the implementation of an e-voting system, as well as for a secure multi-party computation protocol, which allows the computation of some function, while the parties involved may know the result of the computation, but not the input of the other parties involved.
- A Framework for the Cryptographic Verification of Java-like Programs Computer Security Foundations Symposium (CSF), 2012 IEEE 25th
- Proving Correctness and Security of Two-Party Computation Implemented in Java in Presence of a Semi-Honest Sender 13th International Conference on Cryptology and Network Security (CANS)