Most of the C130J Mission Computer Software (which is cited in the article) is written in SPARK - a highly secure, annotated subset of Ada.
- Rod Chapman, PxCS
Cyclone is good, but check out SPARK...
on
C with Safety - Cyclone
·
· Score: 2, Informative
Cyclone is a remarkable achievement, given they
started with C...
MISRA-C is also a good effort, although somewhat
built on sand.
The safety-critical community over here in Europe,
and also a few projects in the USA use SPARK
though, which is a high-integrity, annotated
subset of Ada. It's static analysis tool
is really remarkable - anyone for static proof
of exception freedom? (e.g. static proof of
no buffer overflow for all input data)
Eiffel is also very good from a high-integrity
point of view, and well worth a look. It amazes
me how much effort goes into researching static
analysis of langauges that are simple not designed
for that purpose at all...ah well...
I've worked on high-ITSEC software... I know of
only two products that have achieved an ITSEC E6
rating recently - MULTOS (a smartcard operating system) and the Mondex Purse (an electronic cash application that runs on MULTOS) See
http://www.multos.com/ for some info.
The only programming language that comes anywhere
near meeting the ITSEC requirements is SPARK,
which is well-known is the safety-critical
community here in Europe, but actually has its
roots in security research. See
http://www.sparkada.com/
- Rod Chapman
Slashdot Mirror
Most of the C130J Mission Computer Software (which is cited in the article) is written in SPARK - a
highly secure, annotated subset of Ada.
- Rod Chapman, PxCS
Cyclone is a remarkable achievement, given they
started with C...
MISRA-C is also a good effort, although somewhat
built on sand.
The safety-critical community over here in Europe,
and also a few projects in the USA use SPARK
though, which is a high-integrity, annotated
subset of Ada. It's static analysis tool
is really remarkable - anyone for static proof
of exception freedom? (e.g. static proof of
no buffer overflow for all input data)
Eiffel is also very good from a high-integrity
point of view, and well worth a look. It amazes
me how much effort goes into researching static
analysis of langauges that are simple not designed
for that purpose at all...ah well...
- Rod Chapman
I'd second that - we build mission- and safety-critical systems here, and Ada remains
:-)
our language of choice for that kind of work.
The GNAT frontend for GCC is rather good now.
The GtkAda binding is also excellent - check
out the GNU Visual Debugger (GVD) too see what
it can do.
GNAT has lots of useful libraries and they're
rigidly portable across all the implementations.
I'll now duck under my desk for the torrent
of replies...
- Rod Chapman
I've worked on high-ITSEC software... I know of only two products that have achieved an ITSEC E6 rating recently - MULTOS (a smartcard operating system) and the Mondex Purse (an electronic cash application that runs on MULTOS) See http://www.multos.com/ for some info. The only programming language that comes anywhere near meeting the ITSEC requirements is SPARK, which is well-known is the safety-critical community here in Europe, but actually has its roots in security research. See http://www.sparkada.com/ - Rod Chapman