Back to list of 2003/04 seminars

Abstract for Seminar

Praxis Critical Systems Ltd recently developed a secure certification authority (CA) for smart cards. The CA had to satisfy demanding performance and usability requirements while meeting stringent security constraints. We used a systematic process from requirements elicitation through formal specification, user interface prototyping, rigorous design and coding in SPARK, a secure Ada subset, to ensure that these objectives were achieved. System validation included tool-assisted checking of a formal process design, top down testing system testing with coverage analysis and static analysis of the code. The system uses COTS hardware and software but no reliance is placed on correctness of COTS for critical security properties. We show how a process which achieves normal commercial productivity can deliver a system which is proving highly reliable in daily use, meeting all its throughput and usability goals.

Roderick Chapman received MEng and DPhil degrees from the University of York, England in 1991 and 1995 respectively. He is currently products manager at Praxis Critical Systems, leading the design and development of the SPARK language and toolset. Before joining SPARK team, Rod was involved in the implementation high-integrity real-time and embedded systems, including SHOLIS (the first system implemented to the Def Stan 00-55 SIL4 standard), the Lockheed Martin C130J Mission Computer, and the MULTOS CA. Rod has presented tutorial, papers and panel sessions at many conferences, including SigAda, Ada Europe, and STC, and remains a member of the Ada95 HRG.

Computer Science @ Kent

	Last modified Monday February 16 10:34:49 GMT 2004 Problems with this page? Contact the CS Webmaster
http://www.cs.kent.ac.uk/dept_info/seminars/2003_04/abs_2004_02_10.html