Advanced Search

Content Type

Topics

Publication Date

Certified Binaries for Software Components

Abstract

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.

Cite This Report

Show Citation Formats

SEI

Chaki, Sagar; Ivers, James; Lee, Peter; Wallnau, Kurt; & Zeilberger, Noam. Certified Binaries for Software Components (CMU/SEI-2007-TR-001). Software Engineering Institute, Carnegie Mellon University, 2007. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=8287

IEEE

Chaki. Sagar, Ivers. James, Lee. Peter, Wallnau. Kurt, and Zeilberger. Noam, "Certified Binaries for Software Components," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Report CMU/SEI-2007-TR-001, 2007. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=8287

APA

Chaki, Sagar., Ivers, James., Lee, Peter., Wallnau, Kurt., & Zeilberger, Noam. (2007). Certified Binaries for Software Components (CMU/SEI-2007-TR-001). Retrieved October 23, 2014, from the Software Engineering Institute, Carnegie Mellon University website: http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=8287

CHI

Sagar Chaki, James Ivers, Peter Lee, Kurt Wallnau, & Noam Zeilberger. Certified Binaries for Software Components (CMU/SEI-2007-TR-001). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2007. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=8287

MLA

Chaki, Sagar., Ivers, James., Lee, Peter., Wallnau, Kurt., & Zeilberger, Noam. 2007. Certified Binaries for Software Components (Technical Report CMU/SEI-2007-TR-001). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=8287