BOSTON, 28 March 2007. Joyce L. Tokar, Ph.D., of Pyrrhus Software opened the second day of the 2007 Military Technologies Conference (MTC; www.miltechconference.com), being held in Boston's Hynes Convention Center.
Tokar's presentation, "Correctness by Construction of High-integrity Software," offered up methods of ensuring security and safety in software construction. "Design and code systems with security in mind," Tokar says. "Systems constructed in this way are inherently more secure because they minimize the design flaws and coding errors that attackers can exploit."
Tokar discussed the benefits of SPARK, defined by Wikipedia as "a secure, formally-defined programming language designed to support the development of software used in applications where correct operation is vital either for reasons of safety or business integrity."
A sub-language of Ada95 language, SPARK is designed for safety critical and secure real-time and embedded applications. SPARK overcomes ambiguity, ensures that all rule violations are detectable, enables a formal definition in the software program, and facilitates correctness by construction. SPARK encompasses an Examiner tool, Simplifier tool, Proof Checker tool, and Proof Obligation Summarizer.
Among the military and aerospace projects for which SPARK was used are the Euro Fighter Typhoon, Harrier II SMS, SHOLIS (the first Def Stan 00-55 SIL4 project), and CJ 130J. SPARK also is contributing to the Mondics Smart Card project, involving the Multi-Application Operating System (MULTOS), a smart-card operating system from the MULTOS Certification Authority in Calif.
"A major goal of SPARK is to enable the strengthening of interface definitions so that most errors are found before the program executes," Tokar explains.
