Challenges and applications of assembly level software model checking [Elektronische Ressource] / von Tilman Mehler

Sujets

• Informatik

Informations

• Publié par: technischen_universitat_dortmund
• Publié le: 01 janvier 2005
• Nombre de lectures: 19
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

ChallengesandApplicationsofAssembly Level
SoftwareModelChecking
Dissertation
zurErlangungdesGradeseines
DoktorsderNaturwissenschaften
anderUniversitätDortmund
amFachbereichInformatik
von
TilmanMehler
Dortmund
20052
X
X
X
X
X
X
X
X
X
X
X
X
X
X
X
X
X
X
X
X
X
TagdermündlichenPrüfung:
Dekan/Dekanin: Prof. BernhardSteffen
Gutachter: Dr. StefanEdelkamp,
Prof. KatharinaMorik.
Note: ausgezeichnet
sehrgut
gut
genügendFürmeineEltern.4Acknowledgements
Hereby, I would like to thank my advisor Dr. Stefan Edelkamp, for his excellent guid
ance. Without his various original ideas, his broad theoretical and practical knowledge,
his reviews and moral support, this thesis would not exist. Moreover, I thank Prof. Dr.
Katharina Morik and Dr. Doris Schmedding who agreed to review my thesis. Also, I
want to thank Shahid Jabbar for his support and his reviews. Further acknowledge
ments must go to the German Research Society (DFG) who financially supported my
research through the project Directed Model Checking with Exploration Algorithms of
Artificial Intelligence. Last, but not least, I would like to thank my girlfriend Frida as
wellasmyfriendsandfamilyfortheirmoralsupport.
56Summary
This thesis addresses the application of a formal method called Model Checking to the
domain of software verification. Here, exploration algorithms are used to search for
errors in a program. In contrast to the majority of other approaches, we claim that the
search should be applied to the actual source code of the program, rather than to some
formalmodel.
There are several challenges that need to be overcome to build such a model checker.
First, the tool must be capable to handle the full semantics of the underlying program
minglanguage. Thisimpliesaconsiderableamountofadditionalworkunlesstheinter-
pretation of the program is done by some existing infrastructure. The second challenge
liesintheincreasedmemoryrequirementsneededtomemorizeentireprogramconfigu
rations. Thisadditionallyaggravatestheproblemoflargestatespacesthateverymodel
checkerfacesanyway. Asaremedytothefirstproblem,thethesisproposestouseanex
istingvirtualmachinetointerprettheprogram. Thistakestheburdenoffthedeveloper,
who can fully concentrate on the model checking algorithms. To address the problem of
largeprogramstates,wecallattentiontothefactthatmosttransitionsinaprogramonly
changesmallfractionsoftheentireprogramstate. Basedonthisobservation,wedevise
anincrementalstoringofstateswhichconsiderablylowersthememoryrequirementsof
program exploration. To further alleviate the per state memory requirement, we apply
state reconstruction, where states are no longer memorized explicitly but through their
generatingpath. Anotherproblemthatresultsfromthelargestatedescriptionofapro
gramliesinthecomputationaleffortofhashing,whichisexceptionallyhighfortheused
approach. Based on the same observation as used for the incremental storing of states,
we devise an incremental hash function which only needs to process the changed parts
of the program’s state. Due to the dynamic nature of computer programs, this is not a
trivialtaskandconstitutesaconsiderablepartoftheoverallthesis.
Moreover, the thesis addresses a more general problem of model checking - the state
explosion, which says that the number of reachable states grows exponentially in the
number of state components. To minimize the number of states to be memorized, the
thesis concentrates on the use of heuristic search. It turns out that only a fraction of all
reachable states needs to be visited to find a specific error in the program. Heuristics
can greatly help to direct the search forwards the error state. As another effective way
to reduce the number of memorized states, the thesis proposes a technique that skips
intermediatestatesthatdonotaffectsharedresourcesoftheprogram. Bymergingsev
eral consecutive state transitions to a single transition, the technique may considerably
truncatethesearchtree.
78
The proposed approach is realized in StEAM, a model checker for concurrent C++ pro
grams, which was developed in the course of the thesis. Building on an existing virtual
machine,thetoolprovidesasetofblindanddirectedsearchalgorithmsforthedetection
of errors in the actual C++ implementation of a program. StEAM implements all of the
aforesaid techniques, whose effectiveness is experimentally evaluated at the end of the
thesis.
Moreover, we exploit the relation between model checking and planning. The claim is,
thatthetwofieldsofresearchhavegreatsimilaritiesandthattechnicaladvancesinone
fields can easily carry over to the other. The claim is supported by a case study where
StEAMisusedasaplannerforconcurrentmulti agentsystems.
The thesis also contains a user manual for StEAM and technical details that facilitate
understandingtheengineeringprocessofthetool.Contents
1 Introduction 15
1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.1.1 DeadlySoftwareErrors . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.1.2 ExpensiveSoftwareErrors . . . . . . . . . . . . . . . . . . . . . . . 15
1.1.3 SoftwareEngineeringProcess . . . . . . . . . . . . . . . . . . . . . 16
1.1.4 CallforFormalMethods . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.2 HistoryandGoals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.3 Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2 ModelChecking 21
2.1 ClassicalModelChecking . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.1.1 Graph BasedFormalisms . . . . . . . . . . . . . . . . . . . . . . . . 21
2.1.2 Models,Systems,Programs,Protocols . . . . . . . . . . . . . . . . . 22
2.1.3 DefinitionofModelChecking . . . . . . . . . . . . . . . . . . . . . . 23
2.1.4 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.1.5 TemporalLogics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.1.6 TypesofProperties . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.2 TowardsaFault FreeProtocol . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.2.1 NeedforModelChecking. . . . . . . . . . . . . . . . . . . . . . . . . 26
2.3 ClassicalModelCheckers . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.3.1 SPIN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.3.2 SMV . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.4 ModelCheckingSoftware . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.4.1 TheClassicalApproach . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.4.2 TheModernh . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.4.3 SomeSoftwareModelCheckers . . . . . . . . . . . . . . . . . . . . . 32
3 StateSpaceSearch 39
910 CONTENTS
3.1 GeneralStateExpansionAlgorithm . . . . . . . . . . . . . . . . . . . . . . 39
3.2 UndirectedSearch. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.2.1 Breadth FirstSearch . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.2.2 Depth FirstSearch . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
3.2.3irstIterativeDeepening . . . . . . . . . . . . . . . . . . . . 42
3.3 HeuristicSearch . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
3.3.1 Best firstSearch. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
3.3.2 A* . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
3.3.3 IDA* . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
4 StEAM 47
4.1 TheModelCheckerStEAM . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
4.2 ArchitectureoftheInternetCVirtualMachine . . . . . . . . . . . . . . . . 47
4.3 EnhancementstoIVM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.3.1 StatesinStEAM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.3.2 TheStateDescription . . . . . . . . . . . . . . . . . . . . . . . . . . 51
4.3.3 CommandPatterns . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
4.3.4 Multi Threading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.3.5 Exploration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.4 SummaryofStEAMFeatures . . . . . . . . . . . . . . . . . . . . . . . . . . 57
4.4.1 Expressiveness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
4.4.2 Multi Threading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
4.4.3 Special PurposeStatementsofStEAM . . . . . . . . . . . . . . . . . 58
4.4.4 Applicability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
4.4.5 DetectingDeadlocks . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
4.4.6IllegalMemoryAccesses . . . . . . . . . . . . . . . . . . . 60
4.5 Heuristics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
4.5.1 Error SpecificHeuristics . . . . . . . . . . . . . . . . . . . . . . . . . 63
4.5.2 Structural . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
5 Planningvs. ModelChecking 67
5.1 SimilaritiesandDifferences . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
5.2 RelatedWork. . . . . . . . . . . . . . . . . . . . . .