It's a great museum. They have lots of historically significant crypto devices, including 5 or 6 enigmas machines
of various types. They also have several "used" supercomputers, including a Cray Y-MP, and a the wonderful-looking
Connection Machine CM5.
For high-integrity stuff, we use SPARK (http://www.sparkada.com/)
- a design-by-contract subset of Ada95 that is entirely designed-from-scratch
for verification purposes.
The verification system implements Hoare-logic and is supported by a
theorem prover. Buffer Overflow is only one of many basic correctness
properties that can be verified. Properties that can be verified
are only limited to what can be expressed as an assertion in first-order
logic.
SPARK is a small language (compared to C++ or Java...) but the
depth and soundness of verification is unmatched by anything like
FindBugs, SPLINT, ESC/Java or any of the other tools for the "popular"
languages.
(If you don't know or care what soundness is in the context of static
analysis, then you've probably missed the point of this post...:-) )
- Rod Chapman, Praxis
Slashdot Mirror
It's a great museum. They have lots of historically significant crypto devices, including 5 or 6 enigmas machines of various types. They also have several "used" supercomputers, including a Cray Y-MP, and a the wonderful-looking Connection Machine CM5.
For high-integrity stuff, we use SPARK (http://www.sparkada.com/) - a design-by-contract subset of Ada95 that is entirely designed-from-scratch for verification purposes. :-) )
The verification system implements Hoare-logic and is supported by a theorem prover. Buffer Overflow is only one of many basic correctness properties that can be verified. Properties that can be verified are only limited to what can be expressed as an assertion in first-order logic.
SPARK is a small language (compared to C++ or Java...) but the depth and soundness of verification is unmatched by anything like FindBugs, SPLINT, ESC/Java or any of the other tools for the "popular" languages.
(If you don't know or care what soundness is in the context of static analysis, then you've probably missed the point of this post...
- Rod Chapman, Praxis
>TFA cites a particular NSA biometric identification program which has "0.00" errors per KSLOC.
Results from the NSA project will be reported (for the first time in a public forum)
at the forthcoming ISSSE 2006 conference in March.
- Rod Chapman
(Disclaimer - yes I am one of the authors of the cited paper and one of the designers of SPARK...)
Cool! Please contact us!
- Rod (SPARK Team, Praxis Critical Systems)