Das Nationalinstitut für Standards und Technologie, NIST, ist die US-Bundesbehörde für Standardisierungsprozesse, die unter anderem für die Sicherheit in der Informationstechnik zuständig ist.
Im Rahmen der SATE-VI-Erhebung
untersuchte das Institut Tools zur statischen Analyse vom C-Code.
Im Ergebnis haben nur zwei Tools die NIST-Testkriterien erfüllt: Astrée
und Frama-C.
Astrée wurde auf 28 Sätzen von Benchmarks mit insgesamt 18 954 Fehlern unterschiedlichster Natur getestet. Alle 18 954 wurden von Astrée entdeckt.
Dazu zählten unter anderem arithmetische Überläufe, Pufferüberläufe, ungültige Zeigermanipulationen, Division durch Null, Benutzung uninitialisierter Variablen, mehrfache Deallokation, Endlosschleifen, toter Code und vieles mehr.
Darüberhinaus entdeckte Astrée in den Benchmarks Tausende unbeabsichtigter Fehler.
Der Abschlußbericht des NIST betont Astrées außerordentliche Präzision, sowohl im Hinblick auf die Analyseergebnisse als auch auf das Analysemodell an sich.
“Alarms from Astrée led us to find and fix thousands of mistakes in what was intended as the Juliet known-bug list, manifest.xml.
Because Astrée analyzes code very precisely and we checked meticulously, details of modeling that otherwise would be inconsequential showed up and had to be resolved.”
Der vollständige Bericht wurde in Mai 2020 veröffentlicht
und steht als kostenloser PDF-Download auf der NIST-Webseite zur Verfügung:
nvlpubs.nist.gov/nistpubs/ir/2020/NIST.IR.8304.pdf
Jetzt kostenlos testen
Probieren Sie Astrée auf Ihrem eigenen Code aus, kostenlos und bis zu 30 Tage lang.