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.

By: Matthew Kaplan; Paul A. Karger; Suzanne K. McIntosh; Elaine Palmer; Amitkumar Paradkar; David C. Toll; Sam Weber

Published in: RC24686 in 2008

LIMITED DISTRIBUTION NOTICE:

This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.

rc24686.pdf

Questions about this service can be mailed to reports@us.ibm.com .