Astree: Nachweis der Abwesenheit von Laufzeitfehlern

D. Kästner, C. Ferdinand, S. Wilhelm, S. Nenova, O. Honcharova, A. Miné, X. Rival, L. Mauborgne, E. Sims, J. Feret, P. Cousot, R. Cousot

Description

Niveau: Secondaire, Lycée, Terminale
Astree: Nachweis der Abwesenheit von Laufzeitfehlern Daniel Kastner1, Christian Ferdinand1, Stephan Wilhelm1, Stefana Nenova1, Olha Honcharova1, Patrick Cousot2, Radhia Cousot2, Jerome Feret2, Laurent Mauborgne2, Antoine Mine2, Xavier Rival2, Elodie-Jane Sims2 1 AbsInt GmbH, Saarbrucken, Germany 2 Ecole Normale Superieure, Paris, France 05.06.2009 Kurzzusammenfassung Sicherheitskritische eingebettete Systeme mussen ho- hen Qualitatsanforderungen genugen. Laufzeitfehler, z.B. arithmetische Uberlaufe oder Rundungsfehler konnen zu fehlerhaftem Programmverhalten fuhren. Da in der Regel keine vollstandige Testabdeckung moglich ist, bieten sich statische Analysatoren an. Diese bieten eine vollstandige Coverage, konnen je- doch Fehlalarme erzeugen. Da jeder potentielle Lauf- zeitfehler manuell vom Benutzer uberpruft werden muss, kann eine hohe Zahl von Fehlalarmen dazu fuhren, dass echte Fehler ubersehen werden. Der sta- tische Analysator Astree kann durch Spezialisierung und Parametrisierung an die zu analysierende Softwa- re angepasst werden. Dies ermoglicht kurze Analyse- zeiten und eine niedrige Zahl von Fehlalarmen. Astree wird z.B. bei der Zertifizierung von industrieller Flug- zeugsteuerungssoftware eingesetzt. Schlusselworter Softwarevalidierung, Laufzeitfehler, statische Analyse. 1 Einfuhrung Die Test- und Validierungsphase stellt einen erheb- lichen Kostenfaktor bei der Entwicklung sicherheits- kritischer Systeme dar. Unentdeckte Fehler konnen schwere Schaden verursachen. Daher stellt sich die Frage, wie mit vertretbarem Aufwand das korrek- te Funktionieren der Software nachgewiesen werden kann.

• auf


• ein wichtiges


• nachweis der


• die jeweilige


• abwesenheit von


• laufzeitfeh- ler das


• compileroptmierungen zu


• und berucksichtigt


• astree

Sujets

• Première
• Airbus

Informations

• Publié par: profil-zyan-2012
• Nombre de lectures: 22
• Langue: Deutsch

Extrait

Astr´ee:NachweisderAbwesenheitvonLaufzeitfehlern

1 11 1 DanielKa ¨ stner,ChristianFerdinand,StephanWilhelm,StefanaNenova, 1 2 22 OlhaHoncharova,PatrickCousot,RadhiaCousot,Je´roˆmeFeret, ´ 2 22 2 LaurentMauborgne,AntoineMine´,XavierRival,Elodie-JaneSims 1 AbsIntGmbH,Saarbr ¨ ucken,Germany 2 ´ EcoleNormaleSup´erieure,Paris,France 05.06.2009

Kurzzusammenfassung SicherheitskritischeeingebetteteSystemem ¨ ussenho- henQualit ¨ atsanforderungengen ¨ ugen.Laufzeitfehler, ¨ z.B.arithmetischeUberla ¨ ufeoderRundungsfehler ko ¨ nnenzufehlerhaftemProgrammverhaltenf ¨ uhren. DainderRegelkeinevollst ¨ andigeTestabdeckung mo ¨ glichist,bietensichstatischeAnalysatorenan. Diesebieteneinevollsta ¨ ndigeCoverage,k ¨ onnenje- doch Fehlalarme erzeugen. Da jeder potentielle Lauf- zeitfehlermanuellvomBenutzeru ¨ berpru ¨ ftwerden muss, kann eine hohe Zahl von Fehlalarmen dazu fu ¨ hren,dassechteFehler ¨ ubersehenwerden.Dersta- tischeAnalysatorAstre´ekanndurchSpezialisierung und Parametrisierung an die zu analysierende Softwa- reangepasstwerden.Dieserm ¨ oglichtkurzeAnalyse- zeitenundeineniedrigeZahlvonFehlalarmen.Astr´ee wird z.B. bei der Zertifizierung von industrieller Flug- zeugsteuerungssoftware eingesetzt. Schlu ¨ sselwo ¨ rter Softwarevalidierung, Laufzeitfehler, statische Analyse. 1Einf ¨ uhrung Die Test- und Validierungsphase stellt einen erheb- lichen Kostenfaktor bei der Entwicklung sicherheits- kritischerSystemedar.UnentdeckteFehlerk ¨ onnen schwereScha ¨ denverursachen.Daherstelltsichdie Frage, wie mit vertretbarem Aufwand das korrek- te Funktionieren der Software nachgewiesen werden kann. In der Luftfahrt- und Automobilindustrie wer- den zunehmend statische Analysatoren auf der Ba- sis der Abstrakten Interpretation eingesetzt, um Pro- grammeigenschaften sicherheitskritischer Software zu validieren.Beispielehierfu ¨ rsindderNachweisder l ¨ angstm ¨ oglichenAusfu ¨ hrungszeit[17] und des maxi- malen Stackverbrauchs von Tasks [10], Codeinspek- tion [14], die Bestimmung der Genauigkeit von Gleit- kommaberechnungen [11] und der Ausschluss des Auf- tretens von Laufzeitfehlern [2,6,8]. Moderne stati- sche Analysatoren skalieren gut und erlauben somit dieAnalysevollst ¨ andigersicherheitskritischerIndu- strieanwendungen.

1

Der vorliegende Artikel konzentriert sich auf ei- nebestimmteFehlerklasse,n ¨ amlichdiesogenannten Laufzeitfehlerieftuazffru ¨ heel.L-deinenhrdaelegrR zu, dass nach ihrem Auftreten das Programmverhal- ten undefiniert ist. Einige Laufzeitfehler, z.B. floating- ¨ pointUberl ¨ aufe,ko ¨ nnenInterruptsausl ¨ osenundso- mit abgefangen werden – vorausgesetzt, ein entspre- chender Interrupthandler wurde implementiert. Die mo ¨ glichenFolgenvonLaufzeitfehlernwiebeispiels- weise Feldgrenzenverletzungen beim Zugriff auf Fel- delemente (array access out-of-bounds) oder die Dereferenzierungeinesungu ¨ ltigenZeigersreichenvon fehlerhaftem Programmverhalten bis hin zum Softwa- reabsturz. Ein wichtiges Ziel bei der Entwicklung sicherheits- kritischer Software ist daher der Nachweis, dass kei- nesolchenFehlerzurLaufzeitauftretenko ¨ nnen.Ein Nachweis der Abwesenheit von Laufzeitfehlern kann durch Softwaretests nicht erbracht werden, da in der Regelkeinevollst ¨ andigeTestabdeckungm ¨ oglichist. Mit Hilfe statischer Analyse kann ein solcher Nach- weisselbstf ¨ urgroßeSoftwareprojektegefu ¨ hrtwer- den.EinGrundfu ¨ rdenErfolgstatischerAnaly- setechniken liegt darin, dass sie auf einersicheren ¨ Uberapproximationder konkreten Programmsemantik basieren. Das bedeutet, dass das Ergebnis einer sol- chenAnalysefu ¨ reineAnweisungxentweder”xwird niemalszueinemFehlerfu ¨ hren”oder”xk ¨ onnteeinen Fehler verursachen” lautet. Im ersten Fall ist die Feh- lerfreiheit garantiert, im zweiten Fall liegt entweder ein Fehler vor, oder es handelt sich um einen Fehl- alarm.DieseUnscha ¨ rfeerm ¨ oglichtesstatischenAna- lysatoren,selbstfu ¨ rgroßeSoftwareprojekteinnerhalb akzeptabler Zeit ein Ergebnis zu berechnen. Die Ana- lyseergebnissesindtrotzdemverl ¨ asslich,dasichder Analysator bei korrektem Design nur auf der sicheren Seite irren kann: Wenn die Analyse keinen Fehler fin- det,istderNachweisderFehlerfreiheitgef ¨ uhrt.Die Abdeckung liegt bei 100%. Es stellen sich somit zwei zentrale Anforderun- gen an einen Analysator: Da jede Fehlermeldung u ¨ berpr ¨ uftwerdenmuss,isteszumeinenwichtig,dass derAnalysatorpra ¨ ziseist,d.h.nurwenigeFehlalar-