Soft­ware Cer­ti­fic­a­tion Tools (So­CeTs)

The Software Certification Tools (SoCeTs) are extensions/components of the existing software analysis tool CPAchecker and the SFB 901 service specification environment SSE. The extensions to CPAchecker integrate our proof carrying code and programs-from-proofs approaches. The extension of SSE allows us to transform SSL specifications into inputs for our analysis tools.

Fea­tures

Currently, the software certification tools consists of three components: a component certification for the integration of PCC into CPAchecker, a second component programs-from-proofs integrating PfP concepts into CPAchecker and another component which translates SSL specifications into inputs for the software analysis tool CPAchecker.

Certification

This extension integrates the configurable program certification concept with its current improvements into CPAchecker as well other experimental PCC concepts.

  • Two forms of certificates: abstract reachability graph or set of abstract states
  • Certificate reduction providing different strategies
    • Store only a subset of the abstract states
    • Block abstraction memoization to store similar subproofs only once
  • Certificate compression via ZIP
  • Implementation of certificate validation
  • Parallization of certificate validation based on various strategies
    • Parallel checking
    • Parallel certificate reading
    • Certificate reading and checking in parallel

Programs-from-Proofs

This extension provides the necessary components to provide the PfP concept in CPAchecker.

  • Transformation of program after verification based on abstract reachability graph (ARG)
  • Translation of abstract reachability graph into C program
  • Predicate refinement based on failure of dataflow analyses

SSL Translation

This extension allows the transformation of specification given in the SFB 901 service specification language into the input language of verification tools. The translations are provided as plugins in SSE. Currently, only a translation from protocol specifications into CPAchecker's specification language - a language based on the BLAST query language - is available. Note that the two languages are not identical and a semantics preserving translation is only possible under certain constraints.

Contact

If you have any questions concerning certification in CPAchecker, the integration of programs-from-proofs in CPAchecker or the transformation of SSL specifications into CPAchecker specification, please contact Marie-Christine Jakobs.

Further information:

Projects Project Area A Project Area B Project Area C Project Area T Tools and Demonstration Systems Tools from the 1st Funding Period Tools from the 2nd Funding Period Tools from the 3rd Funding Period