Software Tools


BYODroid is an Android-based implementation of a Secure Meta-Market, allowing to define and enforce formal "Bring Your Own Device" policies on mobile apps. The theoretical background of BYODroid can be found in [SAC2013] and [IJIS2014], while the experimental assessment is discussed in [Computer2014] and [WiSec2014].


The AVANTSSAR Platform The AVANTSSAR Validation Platform, an automated toolset for validating trust and security aspects of service-oriented architectures. An overview of the AVANTSSAR Platform can be found here.


ASASP (short for Automated Symbolic Analysis of Security Policies) is an implementation of the analysis techniques for Administrative RBAC (ARBAC) policies. It implements a symbolic backward reachability analysis to solve user-role reachability problems. An overview of ASASP can be found here.


Eureka is a model checker for sequential software based on the counterexample-guided abstraction refinement (CEGAR) paradigm. Unlike many other software model checkers based on the CEGAR paradigm Eureka analyses arrays precisely. An overview of Eureka can be found here.


SMT-CBMC is a bounded model checker for sequential software. SMT-CBMC reduces the problem of checking whether an input program has an execution path of bounded length violating an assertion to the satisfiability of a formula with respect to a decidable theory. The resulting formula is fed and solved by a state-of-the-art SMT-solver taken off-the-shelf. An overview of SMT-CBMC can be found here.


The AVISPA Tool is a fully automatic analyser for large-scale Internet security-sensitive protocols. It comprises 4 back-ends implementing a variety of security protocol verification techniques. An overview of the AVISPA Tool can be found here.


The AVISS Tool is a fully automatic security protocol analyser. It is capable to analyse a large portion of the protocols collected in the Clark & Jacob library of security protocols. An overview of the AVISS Tool can be found here. The AVISS Tool is the predecessor of the AVISPA Tool.


SATMC (SAT-based Model Checker) is a bounded model checker for security protocols. SATMC reduces the problem of checking whether a protocol is vulnerable to attacks of bounded length to the satisfiability of a propositional formula which is solved by a state-of-the-art SAT solver taken off-the-shelf. SATMC is one of the back-ends of the AVISPA Tool. An overview of SATMC can be found here.


TSAT++ is an open platform for satisfiability modulo theories (SMT) based on a tight coupling of satisfiability procedures and a SAT-solver. The current version of TSAT++ supports Separation Logic (also known as Difference Logic). An overview of TSAT++ can be found here.


RDL (Rewrite and Decision Procedures Laboratory). RDL is a fully automatic tool for formula simplification in a quantifier-free first-order theories. RDL is based on the Constraint Contextual Rewriting paradigm and features a tight integration of rewriting and decision procedures. An overview of RDL can be found here.