Certified Binaries for Software Components
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.
This report is related to the following area(s) of work:
Software AssuranceTechnical Report
CMU/SEI-2007-TR-001
September 2007
Cite This Report
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://www.sei.cmu.edu/library/abstracts/reports/07tr001.cfm
IEEE:
S. Chaki, J. Ivers, P. Lee, K. Wallnau, and N. Zeilberger, "Certified Binaries for Software Components," Software Engineering Institute, Carnegie Mellon University, Pittsburgh, Pennsylvania, Technical Report CMU/SEI-2007-TR-001, 2007. http://www.sei.cmu.edu/library/abstracts/reports/07tr001.cfm
APA:
Chaki, S., Ivers, J., Lee, P., Wallnau, K., & Zeilberger, N. (2007). Certified Binaries for Software Components (CMU/SEI-2007-TR-001). Retrieved May 22, 2013, from the Software Engineering Institute, Carnegie Mellon University website: http://www.sei.cmu.edu/library/abstracts/reports/07tr001.cfm
CHI:
Chaki, Sagar, James Ivers, Peter Lee, Kurt Wallnau, and Noam Zeilberger. Certified Binaries for Software Components (CMU/SEI-2007-TR-001). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2007. http://www.sei.cmu.edu/library/abstracts/reports/07tr001.cfm
MLA:
Chaki, S., Ivers, J., Lee, P., Wallnau, K., & Zeilberger, N. 2007. Certified Binaries for Software Components (Technical Report CMU/SEI-2007-TR-001). Pittsburgh: Software Engineering Institute, Carnegie Mellon University. http://www.sei.cmu.edu/library/abstracts/reports/07tr001.cfm
Find Us Here
Share This Page
For more information
