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. The extensions to CPAchecker integrate our proof carrying code and programs-from-proofs approaches. The proof-carrying code extensions is also part of the OTF Proof-of-Concept.

Former Developers:

  • Marie-Christine Jakobs

Current Developers:

  • Manuel Töws
  • Prof. Dr. Heike Wehrheim

Fea­tures

Currently, the software certification tools consists of two components: a component certification for the integration of PCC into CPAchecker and a second component programs-from-proofs integrating PfP concepts into 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
  • Support of various configuarable program analysis
    • among others interval, information flow, octagon, predicate, reaching definition, sign, uninitilized variables and value analyses
  • Certificate reduction providing different strategies
    • Store only a subset of the abstract states
    • Reduction of stored information (only value analysis)
    • Reduction of property-irrelevant information (only information flow analysis)
  • 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
  • Partialization of certificates
    • Partition of analysis results into several smaller certificates
    • Aggregation of partial certificate validation results during validation

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

&nbs

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 Manuel Töws.