Frustration Strategies: Formal Verification

Beyond the frustration capabilities gained by configuring conventional operating systems and services, it is possible to define a set of security controls that cannot be avoided by users of the computers involved, either authorized users or adversaries. These unavoidable controls are referred to as mandatory security, and are based on the concept of logical proofs of security. This chapter discusses these methods, and applies them to frustrate potential adversaries.