Policies and Proofs for Code Auditing
Source: University of California
Both proofs and trust relations play a role in security decisions, in particular in determining whether to execute a piece of code. The authors have developed a language, called BCIC, for policies that combine proofs and trusted assertions about code. In this paper, using BCIC, they suggest an approach to code auditing that bases auditing decisions on logical policies and tools. Deciding to execute a piece of software can have substantial security implications. Accordingly, a variety of criteria and techniques have been proposed and deployed for making such decisions.