Policies and Proofs for Code Auditing
- Nathan Whitehead ,
- Jordan Johnson ,
- Martin Abadi
Automated Technology for Verification and Analysis (ATVA) |
Published by Springer
Both proofs and trust relations play a role in security decisions, in particular in determining whether to execute a piece of code. We have developed a language, called BCIC, for policies that combine proofs and trusted assertions about code. In this paper, using BCIC, we suggest an approach to code auditing that bases auditing decisions on logical policies and tools.