An attempt to examine the Tokeneer using Bakar Kiasan.

Abstract

In order to demonstrate that developing highly secure systems to the level of rigor required by the higher assurance levels of the common criteria is possible, the NSA asked Praxis High Integrity Systems to undertake a research project to develop a high integrity variant of part of an existing secure system (the Tokeneer System) in accordance with Praxis‟ own high-integrity development process. Their objective is to show the security community that it is possible to develop secure systems rigorously in a cost-effective manner. Hence part of the Tokeneer (ID Station) is redeveloped in Spark programming language and is verified using the Spark proof tools. Bakar Kiasan is a symbolic execution tool for the Spark programming language built in Kansas State University, it can be used for bug finding, test case generation and contract checking. This tool‟s proof process does not include the conventional Spark tools like the Examiner, Simplifier and Proof Checker. It mainly allows the programmer to focus entirely on the source code level. The goal of this MS report is to assess the extent to which symbolic execution techniques in Bakar Kiasan can be applied to the Tokeneer example implemented in Spark.