First results of PCC for assembler programs were already published in 1997 by Necula and Lee. However, while these works mainly deal with type and memory safety properties, we are interested in less restricted classes of functional properties, e.g., pre- and postconditions, reachability of (error) locations and protocols describing allowed sequences of actions like method calls. Especially, subproject B3 relies on grey box service descriptions, e.g., sequences of method calls, during its analyses. Furthermore, we cannot expect that a service provider is familiar with semi-automatic verification techniques like theorem proving and require also a fully automatic verification of these properties. Finally, the main goal of our research is to keep the idea that the majority of the workload is shifted to the provider and we may deviate from the original PCC concept.
Strictly following the PCC idea, we developed a configurable certification framework which can be configured to show any of our functional properties. In contrast to Abstraction-carrying Code developed by Albert et. al. in 2004 which is a PCC framework for arbitrary abstract interpretations we support static analyses, abstract interpretation and model checking considering various abstract domains.
The configurable certification framework is based on the existing configurable program analysis framework from Beyer et. al. implemented in CPAchecker. In the configurable certification framework the provider constructs an abstract state space. In the basic framework, the abstract states are sent to the consumer who recomputes the abstract successors of each state, proves that successors are correctly considered and checks if the desired property is valid. Currently, we are interested in the improvement of this framework:
- How much information must be stored in the certificate?
- How can we parallelize our certificate validation?
- How can we improve the representation of certificates?
- Can we simplify certificate validation?
- Can we support further analyses described in the configurable program analysis framework?
We already developed first approaches tackling the first and second question resulting in performance improvements of the consumer’s tasks. These approaches store a partitioned subset of the abstract state space. They read and validate the certificate in parallel and recompute the missing part of the abstract state space during validation.