This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Lessons Learned Building the Caernarvon High-Assurance Operating System
January/February 2011 (vol. 9 no. 1)
pp. 22-30
Samuel Weber, National Science Foundation
This article features lessons learned in designing, developing, and testing features for a high-assurance smart card operating system. In particular, this paper describes software design, development, and testing process, and the advantages reaped from following established process guidelines. The authors describe the project impact experienced from external influences and count among them market pressure from a rapidly changing commercial landscape which demands agility in order to assure continued funding and product success.

1. Common Criteria for Information Technology Security Evaluation –Parts 1, 2, and 3, version 2.3, CCMB-2005-08-001, CCMB-2005-08-002, and CCMB-2005-08-003, Common Criteria Recognition Arrangement, 2005; www.commoncriteriaportal.orgthecc.html.
2. G. Schellhorn et al., "Verification of a Formal Security Model for Multiapplicative Smart Cards," Proc. 6th European Symp. Research in Computer Security (Esorics 2000), LNCS 1895, Springer, 2000, pp. 17–36.
3. Digital Signature Standard (DSS) with Change Notice 1, FIPS PUB 186-2, with Change Notice 1, 5 Oct. 2001, Jan. 2000, Nat'l Inst. Standards and Technology, 2001, 2000; http://csrc.nist.gov/publications/fips/archive/ fips186-2fips186-2-change1.pdf.
4. P.A. Karger and H. Kurth, "Increased Information Flow Needs for High-Assurance Composite Evaluations," Proc. 2nd IEEE Int'l Information Assurance Workshop, IEEE CS Press, 2004, pp. 129–140.
5. P.A. Karger et al., "A Retrospective on the VAX VMM Security Kernel," IEEE Trans. Software Eng., vol. 17, no, 11, pp. 1147–1165.
6. Multilevel Computer Security Requirements of the World Wide Military Command and Control System (WWMCCS), LCD-78-106, General Accounting Office, 5 Apr. 1978; www.gao.gov/docdblitesummary.php?&rptno=LCD-78-106 .
7. R.R. Schell, "Computer Security: The Achilles' Heel of the Electronic Air Force?" Air Univ. Rev., vol. 30, 1979, pp. 16–33; www.airpower.maxwell.af.mil/airchronicles/ aureview/1979/jan-febschell.html.
8. Certification Report for Tachograph Card Version 1.0 128/64 R1.0 from ORGA Kartensysteme GmbH, BSI-DSZ-CC-0205-2003, Bundesamt für Sicherheit in der Informationstechnik, 22 Aug. 2003; https://www.bsi.bund.de/cae/servlet/contentblob/ 480764/publicationFile/300980205a_pdf.pdf .
9. D.C. Toll et al., "Tooling in Support of Common Criteria Evaluation of a High Assurance Operating System," Build Security In,3 Apr. 2008; https://buildsecurityin.us-cert.gov/daisy/ bsi/articles/knowledge/lessons961.html .
10. D. Hutter et al., "VSE: Controlling the Complexity in Formal Software Developments," Applied Formal Methods − FM-Trends 98: Proc. Int'l Workshop on Current Trends in Applied Formal Methods, LNCS 1641, Springer, 1998, pp. 351–358.
11. G. Kleinet al., "seL4: Formal Verification of an OS Kernel," Proc. 22nd ACM Symp. Operating Systems Principles, ACM Press, 2009; http://ertos.nicta.com.au/publications/papers Klein_EHACDEEKNSTW_09.pdf.
12. D. Brand, "A Software Falsifier," Proc. 11th Int'l Symp. Software Reliability Eng. (ISSRE 00), IEEE CS Press. 2006, pp. 174–185.
13. C. Cadar and D. Engler, "Execution Generated Test Cases: How to Make Systems Code Crash Itself," Model Checking Software: 12th Int'l SPIN Workshop on Model Checking of Software, LNCS 3639, Springer, 2005, pp. 2–23.
14. S. Redwine, "Introduction to Modeling Tools for Software Security," Nat'l Cyber Security Division, US Dept. Homeland Security, 21 Feb. 2007; https://buildsecurityin.us-cert.gov/daisy/ bsi/articles/tools/modeling698.html?branch=1&language=1 .
15. S. Weber, P.A. Karger, and A. Paradkar, A Software Flaw Taxonomy: Aiming Tools At Security, RC 23538 (W0502-133), IBM Research Division, Thomas J. Watson Research Center, 25 February 2005; www.research.ibm.com/resourcespaper_search.html .
16. A. Paradkar et al., "Chicken & Egg: Dependencies in Security Testing and Compliance with Common Criteria Evaluations," Proc. IEEE Int'l Symp. Secure Software Eng. (ISSSE 06), IEEE CS Press, 2006, pp. 65–74.
17. S. Weber et al., "The Feasibility of Automated Feedback–Directed Test Generation: A Case Study of a High-Assurance Operating System," Proc. 19th Int'l Symp. Software Reliability Eng. (ISSRE 08), IEEE CS Press, 2008, pp. 229–238.
18. Enhanced Border Security and Visa Entry Reform Act of 2002, Public Law No. 107–173, 107th Congress, 2nd session, 14 May 2002; http://frwebgate.access.gpo.gov/cgi-bingetdoc.cgi?dbname=107_cong_public_laws&docid=f:publ173.107.pdf .
19. Policy for a Common Identification Standard for Federal Employees and Contractors, Homeland Security Presidential Directive 12, 27 Aug. 2004; http://csrc.nist.gov/drivers/documentsPresidential-Directive-Hspd-12.html .
20. P.Q. Nguyen and I.E. Shparlinski, "The Insecurity of the Digital Signature Algorithm with Partially Known Nonces," J. Cryptography, vol. 15, no. 3, 2008. pp. 151–176.
21. N.A. Howgrave-Graham and N.P. Smart, "Lattice Attacks on Digital Signature Schemes," Designs, Codes and Cryptography, vol. 23, no. 3, 2001, pp. 283–290.
1. H.R. Scherzer et al., "Authenticating Mandatory Access Controls and Preserving Privacy for a High-Assurance Smart Card," Proc. 8th European Symp. Research in Computer Security (ESORICS 03), LNCS 2808, Springer, 2003, pp. 181–200.
2. Application Interface for Smart Cards Used as Secure Signature Creation Devices – Part 1: Basic Requirements, CWA 14890-1, Comité Européen de Normalisation (CEN), Mar. 2004; ftp://ftp.cenorm.be/PUBLIC/CWAs/e-Europe/eSign/cwa14890-01-2004-Mar.pdf.
3. D.C. Toll et al., "The Caernarvon Secure Embedded Operating System," Operating Systems Rev., vol. 42, no. 1, 2008, pp. 32–39.
1. Identification Cards – Integrated Circuit(s) with Contacts, Part 4: Organization, Security, and Commands for Interchange, ISO Std. 7816-4, ISO, 2005.
2. P.A. Karger et al., "Implementing a High-Assurance Smart-Card OS," Financial Cryptography and Data Security, LNCS 6052, Springer, pp. 51–65.
3. P. Kocher, J. Jaffe, and B. Jun, "Differential Power Analysis: Leaking Secrets," Advances in Cryptography: Proc. 19th Ann. Int'l Cryptology Conf. (Crypto 99), LNCS 1666, Springer, pp. 388–397.
4. S. Chari, J.R. Rao, and P. Rohatgi, "Template Attacks. in Cryptographic Hardware and Embedded Systems," Smart Card Research and Advanced Applications: Proc 9th IFIP WG8.8/11.22 Int'l Conf. (CHES 02), LNCS 2523, Springer, pp. 13–28.
5. S. Chari et al., "Designing a Side Channel Resistant Random Number Generator," Smart Card Research and Advanced Application: Proc. 9th IFIP WG8.8/11.2 Int'l Conf. (Cardis 10), LNCS 6035, Springer, pp. 49–64.

Index Terms:
security kernels, specification, tools, privacy, test design, organizational management and coordination,
Citation:
Paul Karger, Suzanne McIntosh, Elaine Palmer, David Toll, Samuel Weber, "Lessons Learned Building the Caernarvon High-Assurance Operating System," IEEE Security & Privacy, vol. 9, no. 1, pp. 22-30, Jan.-Feb. 2011, doi:10.1109/MSP.2010.169
Usage of this product signifies your acceptance of the Terms of Use.