The Air Force Office of Scientific Research has awarded a multi-year contract to Dr. Rose Gamble to investigate formal methods and mechanisms to support the security certification of multi-component software systems. The goal is to create a calculus that accommodates the expression and proof of functional and non-functional properties and requirements related to key model elements of multi-component systems to verify their compliance with security standards. This work builds on existing research to define Security Certification Models (SCMs), extending formal models that represent security certification criteria to assist in verifing system compliance.
A Sample of the Component Protection Policy using a UML profile can be found here.CPP-UML
This research will specify the contribution of several core modeling elements for security policies. The first model element in the resarch is the system of systems (SoS), which includes the participating components, their connections, and constraints on interactions. A second model element is the component specification which includes its exposed interfaces for interaction along with security policy information for authentication, authorization, data protection, audit, non-repudiation, and contingency planning. Another key model element is the security criteria that govern the compliance of the SoS and its components. While some criteria are based on security policy interactions at the component level, the majority must be interpreted from standards and documents that reference multi-component, net-centric software systems. The result of non-compliance with security criteria should coincide with known vulnerabilities and weaknesses. Finally, there is the security meta-model, a byproduct of the certification process that allows for model maintenance when one or more element specifications change.
There are broad scientific and technical merits to the proposed research. Extending formal models to represent security certification criteria is needed to verify compliance. However, these extensions go beyond SoS to large-scale software intensive systems in which hardware and software interfaces must be certified. By establishing a method by which system designers and certifiers can represent certification requirements, compliance assessment is facilitated. Certification requirements become less ambiguous as a common ontology of certification expressions emerges. This foundation can be expanded in a structured, well-defined way to maintain requirements consistency, increase its completeness, and eliminate redundant or subsuming security certification statements.
The research complements the new, net-centric DIACAP (DoD Information Assurance Certification and Accreditation Process) to facilitate certification and recertification efforts. The outcomes from the calculus use can be encapsulated into a format that is stored within the DIACAP Knowledge Service. As information and knowledge become more valuable to attackers, software must provide adequate protection and evidence that an Air Force system is trustworthy. As software development trends progress, additional complexity of dynamic and evolving systems must also be incorporated into certification processes and methods. There must be a fundamental shift in the acceptability of formal methods which in a sense lessen complexity via abstraction, yet provide greater trust in verification results. This shift must accommodate the need for more practical creation and storage of models and their history.
The certification calculus can offer the formal and practical support for design-time certification and also upgrade the certification process to provide on-demand mission certification of software, in which system assurances can be made on the fly when changes occur. This can reduce the vulnerabilities that can result from patching critical systems in order to deploy them to the warfighter.
Security Certification Modeling, AFOSR, 2005-2008
The Air Force Office of Scientific Research has awarded a 3+ year contract to Dr. Rose Gamble to explore Security Certification Modeling for systems of systems. A framework for Security Certification Models (SCMs) has been completed and can be successfully migrated to the DIACAP. The framework consists of a UML Component Security Policy Profile and Policy Interaction Semantics. SCMs have been illustrated using three distinct examples encompassing multiple security policies, constraints, and certification criteria. Expressing certification criteria to adequately determine compliance can benefit from both uniform and detailed terminology. The framework provides a foundation for this terminology through its policy interaction semantics – a detailed definition and resource reference that substantiates each attribute, method, and constraint across multiple policies.
Research during 2006 and 2007 saw the completion of the security certification modeling framework, the instantiation of three distinct examples to show its use in conflict detection, and the uniform expression of specific certification guidelines in domain-specific terms that adhered to framework attributes. The framework is comprised of a UML Component Security Policy Profile and Policy Interaction Semantics. The Component Security Policy Profile specifies in UML the Security Policy Descriptors developed in the first year of the effort. During the past year (the second year of the effort) the Security Policy Descriptors have been assigned attributes, methods, and constraints according to Policy Interaction Semantics that substantiates similar naming conventions that can be distinctly used by different security policy types as needed. Templates for constraints on instantiated policies were outlined to promote flexibility with instantiating a particular security policy type for a specific component. Finally, we have explored the development of a Violation Tree to allow for visual and graphical processing of policy interaction conflicts or clashes and their relationship to risks with respect to confidentiality, integrity, and availability.