Software Engineering Institute

Proof-carrying code (PCC) and certifying model checking (CMC) are two established paradigms for obtaining objective confidence in the runtime behavior of a program. PCC enables the certification of low-level binary code against relatively simple (e.g., memory-safety) policies. In contrast, CMC provides a way to certify a richer class of temporal logic policies, but is typically restricted to high-level (e.g., source) code. In this report, an approach is presented to certify binary code against expressive policies, and thereby achieve the benefits of both PCC and CMC. This approach generates certified binaries from software specifications in an automated manner. The specification language uses a subset of UML statecharts to specify component behavior and is compiled to the Pin component technology. The overall approach thus demonstrates that formal certification technology is compatible with, and can indeed exploit, model-driven approaches to software development. Moreover, this approach allows the developer to trust the code that is produced without having to trust the tools that produced it. In this report details of this approach are presented and experimental results on a collection of benchmarks are described.