Satisfying Common Criteria Security Evaluation Testing Requirements: Two Case Studies Using a High-Assurance Operating System

In this paper, we describe results of two case studies designed to satisfy the testing requirements mandated by higher levels of the Common Criteria for security evaluations. These requirements include 1) Demonstrable independence of individual test cases 2) Demonstrable coverage of both user level specifications and implementation code. The case studies are based on a highly secure smart card operating system. In the first case study, we used automated specification based test generation, together with fault injection, to demonstrate that self-contained test cases are independent and do not lead to fault masking. The goal of the second case study was to demonstrate adequate code coverage, while retaining the ability to generate expected outputs based on specifications. To that end, we first established mappings between the specification and implementation code elements. Test cases were then generated from the user level specification to identify the executed code elements and we attempted to use static analysis to map the unexecuted code elements to the corresponding elements in the user level specification. In this second case study, we found that, given a sufficiently expressive user level specification, and a test generation system that is able to effectively use such a specification, the resulting tests will cover the vast majority of the code branches that are able to be covered. Therefore, the benefit of a feedback-directed system will be limited. We further provide evidence that the static analysis required to generate feedback in these cases tends to be difficult, involving inferring the semantics of the internal implementation of data structures. In particular, we observed that the internal states at the implementation level in a high security application pose significant challenges to this mapping process.