Reliably Secure Software Systems (RS3) –
DFG Priority Programme 1496

Tools developed or improved within RS3 projects

Tools developed within RS3 Reference Scenarios

  • Security in E-Voting
    sElect: sElect is a new remote E-Voting system for elections. Security is critical for E-Voting: Within RS3, we developed the first E-Voting system that comes with formal guarantees of security on the implementation level. These guarantees have been proven with a novel combination of techniques from cryptography and program verification, using the state-of-the-art tools Joana and KeY for analysis of Java programs.
  • Security in Web-based Workflow Management Systems
    CoCon: CoCon is a verified conference management system. It has already been used successfully used in the submission-review-notification process of the Isabelle 2014 workshop. The system proved to be functional. The tool can be found here.
  • Software Security for Mobile Devices
    RS3 Certifying App Store: The RS3 Certifying App Store is a tool that supports users of Android mobile devices in installing secure apps. To this end, the RS3 Certifying App Store integrates different tools and approaches developed in RS3: the model-driven development approach from the IFlow project, the static RSCP security analyser from the RSCP project, and the dynamic enforcement tool DroidForce from the projects SADAN and RUNSECURE. An initial prototype of the RS3 Certifying App Store integrating the three aforementioned approaches has already been developed.

Program Analysis Tools

  • Project ALBIA
    Standalone Verifier for IF Properties: The standalone verifier automatically generates loop invariants using a novel approach on integrating abstraction into a logic framework. See here for more details.
    Exploit Generation: Generates exploits for information leaks. Supported Policies: non-interference and delimited information release. Supported arithmetics: Integer arithmetic. Supported operators: addition, subtraction and multiplication. See here for more details.
  • Project DeduSec
    dsharp-p: dsharp-p is a #SAT solver/propositional model enumerator equipped with projection. This tool is part of a tool chain for quantitative analysis of information flow in ANSI C programs, based on SAT/#SAT.
  • Project IFC4MC
    Program Analysis framework for information flow control for Java Programs. Joana can handle full Java with arbitrary threads. Joana discovers explicit, implicit, and probabilistic leaks. Joana uses a stack of modern program analysis methods to achieve high precision. See here for more details.
  • KeY: The KeY system is a system for formal verification and analysis of Java programs. For more details, see here.
    KeY-IFC: KeY-IFC is a system for program-level specification and deductive verification of information-flow properties of Java programs. For more details, see here.