Verifying compliance of trusted programs

摘要: In this paper, we present an approach for verifying that trusted programs correctly enforce system security goals when deployed. A program is to only perform safe operations despite have the authority unsafe operations; example, initialization programs, administrative root network daemons, etc. Currently, these are without concrete justification. The emergence of tools building guarantee policy enforcement, such as security-typed languages (STLs), and mandatory access control systems, user-level servers, finally offers a basis justifying trust in programs: can determine whether be deployed compliance with reference monitor concept. Since policies defined independently, often using different models, all deployments may difficult achieve practice, however. We observe integrity must dominate data, use insight, which call PIDSI approach, infer relationship between policies, enabling automated verification. find consistent SELinux its programs. As result, designed independently their target yet still manner ensures enforcement goals.