Trust

Administrator installs patch

1.Trusts patch came from vendor, not tampered with in transit

2.Trusts vendor tested patch thoroughly

3.Trusts vendor’s test environment corresponds to local environment

4.Trusts patch is installed correctly

Trust in Formal Verification

•Gives formal mathematical proof that given input i, program P produces output o as specified

•Suppose a security-related program S formally verified to work with operating system O

•What are the assumptions?

Trust in Formal Methods

1.Proof has no errors

•Bugs in automated theorem provers

2.Preconditions hold in environment in which S is to be used

3.S transformed into executable S¢ whose actions follow source code

–Compiler bugs, linker/loader/library problems

4.Hardware executes S¢ as intended

–Hardware bugs (Pentium f00f bug, for example)