An attempt to examine the Tokeneer using Bakar Kiasan.

K-REx Repository

Show simple item record Earlapati, Hari Hara Kumar 2011-08-12T20:54:20Z 2011-08-12T20:54:20Z 2011-08-12
dc.description.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. en_US
dc.language.iso en_US en_US
dc.publisher Kansas State University en
dc.subject Kiasan en_US
dc.subject Spark en_US
dc.title An attempt to examine the Tokeneer using Bakar Kiasan. en_US
dc.type Report en_US Master of Science en_US
dc.description.level Masters en_US
dc.description.department Department of Computing and Information Sciences en_US
dc.description.advisor John M. Hatcliff en_US
dc.subject.umi Computer Science (0984) en_US 2011 en_US August en_US

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search K-REx


My Account


Center for the

Advancement of Digital