If we have a program with strict control flow security requirements and want to ensure system requirements by verifying properties of said program, but part of the code base is in the form of a plug-in or third party library which we do not have access to at the time of verification, the procedure presented in this thesis can be used to generate the requirements needed for the plug-ins or third party libraries that they would have to fulfil in order for the final product to pass the given system requirements. This thesis builds upon a transformation procedure that turns control flow properties of a behavioural form into a structural form. The control flow properties focus purely on control flow in the sense that they abstract away any kind of program data and target only call and return events. By behavioural properties we refer to properties regarding execution behaviour and by structural properties to properties regarding sequences of instructions in the source code or object code. The result presented in this thesis takes this transformation procedure one step further and assume that some methods (or functions or procedures, depending on the programming language) are given in the form of models called flow graph, while the remaining methods are left unspecified. The output then becomes a set of structural constraints for the unspecified methods, which they must adhere to in order for any completion of the partial flow graph to satisfy the behavioural formula. / Om vi har ett program med strikta kontrollflödeskrav och vill garantera att vissa systemkrav uppfylls genom att verifiera formella egenskaper av detta program, samtidigt som en del av kodbasen är i form av ett plug-in eller tredjeparts-bibliotek som vi inte har tillgång till vid verifieringen, så kan proceduren som presenteras i detta examensarbete användas för att generera de systemkrav som de plug-in eller tredjeparts-bibliotek behöver uppfylla för att slutprodukten ska passera de givna systemkraven. Detta examensarbete bygger på en transformationsprocedur som omvandlar kontrollflödesegenskaper på en beteendemässig form till en strukturell form. Kontrollflödes-egenskaperna fokuserar uteslutande på kontrollflöden i den meningen att de abstraherar bort all form av programdata och berör enbart anrop- och retur-händelser. Med beteendemässiga egenskaper syftar vi på egenskaper som berör exekverings-beteende och med strukturella egenskaper syftar vi på egenskaper som berör ordningen på instruktionerna i källkoden eller objektkoden. Resultatet i detta examensarbete tar denna transformationsprocedur ett steg längre och antar att vissa metoder (eller funktioner eller procedurer beroende på programmeringsspråk) är redan givna i formen av modeller som kallas flödesgrafer, medan resten av metoderna fortfarande är ospecificerade. Utdata blir då en mängd av strukturella restriktioner för de ospecificerade metoderna, som de måste följa för att en fulländning av den partiella flödesgrafen ska satisfiera den beteendemässiga formeln.
| Identifer | oai:union.ndltd.org:UPSALLA1/oai:DiVA.org:kth-210843 |
| Date | January 2017 |
| Creators | Björkman, Carl |
| Publisher | KTH, Teoretisk datalogi, TCS |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | English |
| Type | Student thesis, info:eu-repo/semantics/bachelorThesis, text |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.002 seconds