Search

status: published

The importance of security and reliability of software systems makes formal methods of paramount significance for guaranteeing that a system satisfies a particular specification. Hyperproperties can be seen as an abstract formalization of security policies. Because of this, it is desirable to establish a generic verification methodology for at least the class of security-relevant hyperproperties. Unfortunately, such a generic verification methodology is lacking. This is the main motivation of this dissertation.We observe that most interesting hyperproperties that are relevant in practice come from a class of security-relevant policies, specified using universal and possibly existential quantification on traces, as well as relations on those traces. We formalize such definitions and call them holistic hyperproperties. Then our goal becomes to find a methodology for the verification of holistic hyperproperties. To that end, we explore an incremental, coalgebraic perspective on systems and specifications and as a result we arrive at a different, but related kind of specifications: incremental hyperproperties (essentially coinductive predicates). Given some holistic hyperproperty H, the respective incremental version is called H′ and its definition naturally gives the notion of an H′-simulation relation. Such relations enable verification of holistic hyperproperties: finding an H′-simulation relation on a candidate system implies that the incremental hyperproperty H′ holds and thus the high-level, holistic hyperproperty H holds for the candidate system. We also introduce techniques that are often helpful in translating holistic hyperproperties into incremental ones.To show that incremental hyperproperties are important in practice, we explore their connection with the most closely related verification technique via unwinding. To achieve this, we propose a framework for coinductive unwinding of security relevant hyperproperties based on Mantel s MAKS framework and our work on holistic and incremental hyperproperties. Mantel s MAKS framework cannot be used directly as it is geared towards reasoning about finite behavior and is thus not suitable to reason about holistic hyperproperties in general. However, our framework has a similar structure to MAKS: coinductive unwinding relations compose (or imply) coinductive Basic Security Predicates, which in turn compose a number of security-relevant, holistic hyperproperties. It turns out that the coinductive unwinding relations we introduce are instances of H′-simulation relations. More importantly, incremental hyperproperties can be expressed in well-behaved logics and this opens the door to their verification.Finally, we propose a generic verification approach for incremental hyperproperties via game-based model checking. To achieve this, we first show how to interpret incremental hyperproperty checking as games. Although one might do regular model checking of incremental hyperproperties on a transformed system, model checking games are advantageous as they do not only produce a yes-no answer, but also give more intuition about the security policy and what can potentially go wrong, by producing a concrete winning strategy. In order to show that the theory developed here is practical, we present and illustrate methods of using several off-the-shelf tools for verification of incremental hyperproperties expressed in the polyadic modal mu-calculus. nrpages: 198 status: published

Not only does our software grow larger and more complex, we also become more dependent on it, thus making it all the more necessary to develop tools that assist us in writing correct programs. As a consequence, much research has been done in the field of static verification, i.e. the development of algorithms that analyse source code and determine whether it contains certain kinds of errors. This can range from checking that no null dereferences can occur at runtimeto full functional correctness.Verification algorithms, however, are just as much subject to mistakes. Therefore, it is important to put these algorithms under scrutiny: our trust in software can only be as strong as the confidence we can have in our verification tools. In a first step, we closely examine some existing approaches to verification. More specifically, we fully formalise the verification algorithms and prove their soundness.If we are not willing to trust our software nor our verification algorithms, one can wonder why we should trust our formalisations and proofs. For this reason, we also provide full Coq implementations of all verification algorithms we consider, and, for most of them, machine check the soundness proofs.This thesis is divided into two parts. In the first part, we discuss verification condition generation. This approach consists of deriving a logical formula (called verification condition) from a program's source code, whose validity implies the correctness of the program with respect to given specifications. Three such algorithms are investigated, namely the strongest postcondition, the weakest liberal precondition and the weakest precondition. Extra attention is given to the weakest precondition algorithm. In its classic form, it produces a verification condition that grows exponentially with respect to the size of the program. An alternative formulation is available which generates a verification condition that grows only polynomially, but requires the program to be passive, i.e. to not contain any assignments. Fortunately, it is possible to transform any program into an equivalent passive form.We implement this transformation in Coq as well as the more efficient variant of the weakest precondition algorithm, and we provide fully machine checked proofs that this approach is sound.In the second part of the thesis, we turn our attention to symbolic execution. This approach consists of abstractly interpreting the program in such a way that all possible execution paths are considered simultaneously. Verification succeeds if no errors are encountered during this execution.Based on this technique we develop Featherweight VeriFast, representing the core part of VeriFast, an existing verifier developed at the KU Leuven. Featherweight VeriFast is formally defined as a denotational semantics, but it has been implemented in Coq and is extractable, making it usable as a standalone verifier.Featherweight VeriFast's formalisation is built on top of three abstraction layers. The first layer, the result algebra, allows us to reason about angelic and demonic choices, both needed to express the result of a symbolic execution. The second layer defines operators, composable monadic functions which allow us to elegantly deal with the two kinds of nondeterminism and state in a purely functional setting. The third layer provides basic operators, which together form a domain specific language, abstracting away the details of the result algebra. The symbolic execution, central to Featherweight VeriFast's operation, is then defined in terms of these basic operators. Finally, we also provide a (partially machine checked) soundness proof for Featherweight VeriFast. A last chapter discusses verification automation techniques. Some verifiers, for example VeriFast, require the code to be annotated (with for example routine contracts or loop invariants) to be able to determine a program's correctness. Generating these annotations automatically can dramatically decrease the effort required to verify programs. We discuss and compare three different automation techniques. Lastly, we propose a framework in which automation techniques can be added without compromising the soundness of the verification. 1 Introduction 1 1.1 Static Verification Of Imperative Programs 1.2 Overview of Contributions 1.3 Summary I Verification Condition Generation 2 Overview 3 Phase I: From Source to Intermediate Language 13 3.1 BoogiePL 3.2 Source Language 3.2.1 Syntax 3.2.2 Typing 3.2.3 Operational semantics 3.2.4 Modularisation 3.3 Translation 3.3.1 Logical Part 3.3.2 Procedural Part 4 Formal Semantics of the Intermediate Verification Language 4.1 Syntax 4.2 Operational Semantics 4.3 Conclusion 5 Phase II: Generating Verification Conditions 5.1 Hoare Logic 5.2 Strongest Postcondition 5.3 Weakest Liberal Precondition 5.4 Weakest Precondition 5.5 Conclusion 6 Efficient Weakest Preconditions 6.1 Single Assignment Form 6.2 Passification 6.3 EfficientWeakest Preconditions 6.4 Soundness and Size 6.5 Conclusion II Symbolic Execution and Separation Logic 7 Introduction 8 VeriFast Introduction 8.1 Separation Logic 8.1.1 Rationale 8.1.2 Separating Conjunction and Frame Rule 8.2 VeriFast: Hands On 8.2.1 Basics 8.2.2 User Defined Predicates 8.2.3 Recursive User Defined Predicates 8.2.4 List Reversal 8.2.5 Ambiguous Matches 8.3 Related Verification Tools 8.4 Conclusion 9 Featherweight VeriFast 9.1 Small Imperative Language 9.2 Overview 9.3 Result Algebra 9.3.1 Examples 9.3.2 Operations and Axioms 9.3.3 Lemmas 9.4 Operators 9.5 Basic Operators 9.6 Result Algebra Models 9.6.1 Inductive Formulae 9.6.2 Weakest Preconditions 9.7 Operator Lemmas 9.8 Concrete Execution 9.8.1 Formalisation 9.8.2 Shortcomings 9.9 Semiconcrete Execution 9.9.1 Formalisation 9.9.2 Relation with Concrete Execution 9.10 Symbolic Execution 9.10.1 Formalisation 9.10.2 Relation with Semiconcrete Execution 9.10.3 Relation with Concrete Execution 9.11 Conclusion 10 Automation 10.1 General Approach And Rationale 10.2 Working Example 10.3 Auto-open and Auto-close 10.4 Autolemmas 10.5 Shape Analysis 10.6 Comparison 10.7 Conclusion 11 Conclusion and Future Work 11.1 Summary 11.2 Verification Condition Generation vs Symbolic Execution 11.2.1 Similarities 11.2.2 Performance 11.3 RelatedWork 11.3.1 Verification Condition Generation 11.3.2 Symbolic Execution and Separation Logic 11.4 Future Work 11.4.1 Further Formalisation of Verification Condition Generation 11.4.2 Featherweight VeriFast 11.4.3 VeriFast 11.4.4 Reflection nrpages: 482 status: published

Het beveiligen van een groot softwaresysteem is een bijzonder moeilijke opdracht. Uit de ervaring met desktop- en servercomputers weten we dat de onveiligheid van een systeem meestal proportioneel is met een aantal dingen, waaronder de grootte van het aanvalsoppervlak (d.w.z. hoe makkelijk het is voor een aanvaller om te `spreken' met de computer) en hoeveel vrijheid de gebruiker krijgt om applicaties te installeren en uit te voeren.Mobiele telefoons maken momenteel een bijzonder snelle evolutie mee, waardoor ze vaker als doelwit gezien worden voor aanvallers. In een tijdspanne van slechts enkele jaren zijn mobiele telefoons geëvolueerd van een elektronische baksteen die enkel gebruikt kon worden om te bellen en om berichtjes te sturen, tot een hoogtechnologisch multimediatoestel, waarmee gebruikers kunnen surfen op het internet, films en muziek afspelen, foto's nemen, navigeren door het verkeer, en applicaties installeren. Alhoewel dit een bijzonder interessante evolutie is, brengt ze ook een aantal praktische problemen met zich mee. Omwille van de vele extra functies wordt het ook makkelijker voor aanvallers om een beveiligingslek te vinden dat kan misbruikt worden. Daarnaast zijn de verschillende beveiligingsmaatregelen vaak niet meegeëvolueerd.Het hoofdopzet van deze thesis is om de huidige stand van de techniek te verbeteren op vlak van beveiligingsmechanismen tegen aanvallen op mobiele toestellen. Dit kan bereikt worden op twee verschillende manieren. Bestaande software kan beveiligd worden door het incorporeren van nieuwe beveiligingstechnieken. Dit heeft als voordeel dat het slechts een kleine moeite vergt om bestaande software te updaten, maar deze aanpak heeft ook zijn beperkingen. Een andere optie is om de software volledige te herschrijven. Dit kan leiden tot veiligere programmacode, maar vereist wel veel meer werk. Echter, vooraleer oplossingen voor diverse beveiligingsproblemen aangedragen worden, moet eerst aangetoond worden dat mobiele toestellen wel degelijk kwetsbaar zijn.Deze thesis beschrijft drie contributies.1) Alfanumerieke en Turingvolledige ShellcodeWe tonen aan dat een aanvaller die een code-injectie-aanval uitvoert, waarbij hij zeer gelimiteerd is in het type van data dat hij kan gebruiken, nog altijd arbitraire code kan uitvoeren. Beveiligingssystemen die speciale gevaarlijke patronen proberen te detecteren kunnen op deze manier omzeild worden, zonder de mogelijkheden van de aanvaller te beperken. We tonen aan dat voor de ARM-architectuur de subset van instructies die bestaan uit alfanumerieke karakters Turingvolledig is. Een aanvaller die enkel gebruik kan maken van dergelijke alfanumerieke instructies is dus niet gelimiteerd in computationele mogelijkheden.2) Een Tegenmaatregel voor Code-injectie-aanvallenWe stellen een nieuwe tegenmaatregel voor die beschermt tegen code-injectie-aanvallen. Een aangepaste compiler zal extra veiligheidscontroles genereren tijden de compilatie van een C-applicatie. Deze controles maken gebruik van een maskeermechanisme dat verzekert dat codewijzers niet naar geheugenadressen kunnen verwijzen waar ze niet naar zouden mogen verwijzen. Indien een aanvaller erin slaagt om nieuwe programmacode in het geheugen van een applicatie te injecteren, zal het maskeermechanisme voorkomen dat de aanvaller de geinjecteerde code kan uitvoeren.3) Een Implementatie en Evaluatie van Security-by-ContractWe hebben een implementatie gemaakt en geëvalueerd van het nieuwe Security-by-Contract (SxC) paradigma op het volledige en het compacte .NET Framework. Het SxC-raamwerk probeert statisch te garanderen dat een applicatie nooit misbruik zal maken van de beschikbare systeembronnen. Als deze garantie niet statisch gegeven kan worden, dan zal het raamwerk extra beveiligingschecks in de code van de applicatie verweven die ervoor zorgen dat misbruik nooit kan voorkomen.Zoals de evaluatie aantoont, zijn onze beveiligingsmechanismen heel performant en zeer compatibel met bestaande code. De code-injectietegenmaatregel heeft een performantieoverhead van een paar percenten, en heeft een geheugenoverhead van bijna nul percent. Het is zeer compatibel met bestaande code, zoals aangetoond door de SPEC benchmark. De SxC-implementatie deelt dezelfde karakteristieken. Als het systeem statisch kan aantonen dat een applicatie nooit de systeembronnen zal misbruiken, dan zorgt het SxC-systeem voor geen enkele performantie- of geheugenoverhead. Bij applicaties waar dat niet aangetoond kan worden, zullen extra beveiligingschecks worden ingeweven. De overhead van deze extra checks zijn bijna volledig afhankelijk van de complexiteit van de regels die moeten afgedwongen worden. De SxC-implementatie is heel compatibel met bestaande code; er is geen enkele applicatie gevonden die niet bleek te werken met het prototype. Abstract iii Acknowledgements vii Contents ix 1 Challenges in Mobile Phone Security 1 1.1 The Importance of Mobile Phone Security . . . . . . . . . . . . . . 1 1.2 Challenges . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 Goals and Approach . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.4 Context and Technical Challenges . . . . . . . . . . . . . . . . . . 5 1.5 Assumptions and Attack Model . . . . . . . . . . . . . . . . . . . . 6 1.6 Main Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.6.1 Alphanumeric and Turing Complete Shellcode . . . . . . . 7 1.6.2 A Countermeasure against Code Injection Attacks . . . . . 8 1.6.3 An Implementation and Evaluation of Security-by-Contract 8 1.6.4 Other Contributions . . . . . . . . . . . . . . . . . . . . . . 9 1.7 Structure of this Dissertation . . . . . . . . . . . . . . . . . . . . . 10 2 Background 11 2.1 The ARM Architecture . . . . . . . . . . . . . . . . . . . . . . . . 12 2.1.1 Registers . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.1.2 Instructions . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.1.3 Function Calls . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.1.4 Addressing Modes . . . . . . . . . . . . . . . . . . . . . . . 13 2.1.5 Conditional Execution . . . . . . . . . . . . . . . . . . . . . 15 2.1.6 Thumb Instructions . . . . . . . . . . . . . . . . . . . . . . 16 2.2 Code Injection Attacks . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.2.1 Stack-based Buffer Overflows . . . . . . . . . . . . . . . . . 17 2.2.2 Countermeasures and Advanced Attacks . . . . . . . . . . . 19 2.3 Mobile Security Architectures . . . . . . . . . . . . . . . . . . . . . 21 2.3.1 Application Signing . . . . . . . . . . . . . . . . . . . . . . 22 2.3.2 Sandboxing with Virtual Machines . . . . . . . . . . . . . . 23 2.3.3 The Mobile Information Device Profile . . . . . . . . . . . . 24 2.3.4 Android’s Permissions-based Scheme . . . . . . . . . . . . . 25 2.3.5 Advanced Security Architectures . . . . . . . . . . . . . . . 26 3 Filter-resistant Shellcode 27 3.1 Alphanumeric Instructions . . . . . . . . . . . . . . . . . . . . . . . 28 3.1.1 Registers . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.1.2 Conditional Execution . . . . . . . . . . . . . . . . . . . . . 29 3.1.3 The Instruction List . . . . . . . . . . . . . . . . . . . . . . 30 3.1.4 Self-modifying Code . . . . . . . . . . . . . . . . . . . . . . 34 3.2 Writing Shellcode . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 3.2.1 Conditional Execution . . . . . . . . . . . . . . . . . . . . . 35 3.2.2 Registers . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 3.2.3 Arithmetic Operations . . . . . . . . . . . . . . . . . . . . . 38 3.2.4 Bitwise Operations . . . . . . . . . . . . . . . . . . . . . . . 39 3.2.5 Memory Access . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.2.6 Control Flow . . . . . . . . . . . . . . . . . . . . . . . . . . 40 3.2.7 System Calls . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.2.8 Thumb Mode . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.3 Proving Turing-Completeness . . . . . . . . . . . . . . . . . . . . . 44 3.3.1 Initialization . . . . . . . . . . . . . . . . . . . . . . . . . . 46 3.3.2 Parsing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 3.3.3 BF Operations . . . . . . . . . . . . . . . . . . . . . . . . . 47 3.3.4 Branches and System Calls . . . . . . . . . . . . . . . . . . 47 3.4 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 3.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 4 Code Pointer Masking 51 4.1 Design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 4.1.1 Masking the Return Address . . . . . . . . . . . . . . . . . 53 4.1.2 Mask Optimization . . . . . . . . . . . . . . . . . . . . . . . 55 4.1.3 Masking Function Pointers . . . . . . . . . . . . . . . . . . 56 4.1.4 Masking the Global Offset Table . . . . . . . . . . . . . . . 57 4.1.5 Masking Other Code Pointers . . . . . . . . . . . . . . . . . 57 4.2 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 4.2.1 Return Addresses . . . . . . . . . . . . . . . . . . . . . . . . 58 4.2.2 Function Pointers . . . . . . . . . . . . . . . . . . . . . . . . 60 4.2.3 Global Offset Table Entries . . . . . . . . . . . . . . . . . . 60 4.2.4 Limitations of the Prototype . . . . . . . . . . . . . . . . . 62 4.3 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 4.3.1 Compatibility, Performance and Memory Overhead . . . . . 62 4.3.2 Security Evaluation . . . . . . . . . . . . . . . . . . . . . . 63 4.4 Discussion and Ongoing Work . . . . . . . . . . . . . . . . . . . . . 67 4.5 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 4.6 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 5 Security-by-Contract 71 5.1 General Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 5.1.1 Policies and Contracts . . . . . . . . . . . . . . . . . . . . . 72 5.1.2 Enforcement Technologies . . . . . . . . . . . . . . . . . . . 75 5.1.3 Developing SxC Applications . . . . . . . . . . . . . . . . . 77 5.2 S3MS.NET . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 5.2.1 Policy Management and Distribution . . . . . . . . . . . . . 81 5.2.2 Application Deployment and Loading . . . . . . . . . . . . 82 5.2.3 Execution Monitoring and Runtime Enforcement . . . . . . 83 5.3 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 5.4 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 5.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 6 Conclusion 91 6.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 6.2 Ongoing Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 6.3 Future Challenges . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 A Alphanumeric ARM Instructions 97 Bibliography 101 Curriculum Vitae 115 Relevant Publications 117 nrpages: 134 status: published

A static type system is an important tool in efficiently developing correct software. We describe the theoretical underpinnings as well as the practical side of our extension of Scala's type system. More concretely, we generalised Scala's support for parametric polymorphism -- typically called "genericity" in object-oriented languages -- to the higher-order case. We call the result "type constructor polymorphism", as Scala programmers may now safely abstract over type constructors. This generalisation, amplified by the synergy with Scala's existing features such as implicits, represents an important asset in the library designer's abstraction-building tool belt, while the user of these abstractions need not worry about their inner workings. The theoretical side of the story focusses on the lacunae in the existing Scala formalisms, and presents our core calculus that solves these. Finally, we elaborate on our vision for future improvements of the type system, based on our practical experience with type constructor polymorphism. status: published

De tendens van een almaar prominentere computerisatie van onze samenlevi ng manifesteert zich, bijvoorbeeld, in de ontwikkeling van toepassingen voor de overheid en gezondheidszorg. We dienen echter voor ogen te houde n dat deze computerisatie niet alleen aanleiding geeft tot een grotere a utomatisatie en efficientie, maar ook het risico op misbruik op grote sc haal verhoogt. Het is daarom cruciaal dat deze toepassingen beveiligd wo rden door alleen correct gebruik toe te staan. Dit correct gebruik wordt gespecificeerd in een beleid dat vastlegt wanneer een toegang tot een o bject (zoals data of functionaliteit) moet worden ingewilligd of geweige rd. Dit beleid wordt afgedwongen door middel van toegangscontrole. De ge voeligheid van de data die wordt verwerkt, is doorgaans zo hoog dat toeg ang tot deze data gelimiteerd moet worden tot het strikte minimum. Het a fdwingen van een expressief toegangscontrolebeleid wordt des te cruciale r naarmate de organisatie de interne infrastructuur ter beschikking stel t aan buitenstaanders, zoals bijvoorbeeld klanten en leveranciers. Om ee n dergelijk expressief beleid te kunnen afdwingen, dient de gebruikte to egangscontroletechnologie ondersteuning te bieden voor contextgebaseerde toegangscontrole, waarbij een toegangscontrolebeslissing wordt genomen op basis van informatie omtrent de context van de toegangsaanvraag. Voor beelden van contextinformatie zijn de toestand waar de toepassing zich i n bevindt, en de omstandigheden waarin een toegang wordt aangevraagd. De complexiteit en de grootschaligheid van huidige software systemen maakt het moeilijk een toegangscontrolebeleid op uniforme wijze af te dwingen in de toepassingen die draaien binnen de organisatie. Bovendien wordt d eze uniformiteit ondermijnd door een voortdurende evolutie van het toega ngscontrolebeleid en de toegangscontrolelogica. Toegangscontroletechnolo gieen dienen ondersteuning te bieden voor een aanpasbare toegangscontrol e om tegemoet te komen aan de veranderlijke vereisten. Een evaluatie van state-of-the-art technologieen toont aan dat deze technologieen er niet in slagen om een contextgebaseerd beleid op een uniforme en aanpasbare manier af te dwingen. Aan de basis hiervan ligt het onvermogen om het af dwingen van een contextgebaseerd beleid te modulariseren. De oplossing die wij voorstellen, kan worden beschreven in termen van vo lgende twee contributies, namelijk (1) de definities van de concepten ac cess interface en view connector, en (2) de ontwikkeling van een toegang scontroledienst. Een access interface ondersteunt het afdwingen van een contextgebaseerd toegangscontrolebeleid op een uniforme en gecentraliseerde manier in een aantal toepassingen. Deze access interface is een voorstelling van een domeinmodel in termen van de voor toegangscontrole gebruikelijke abstrac ties object - principaal - actie en omvat enkel de informatie die nodig is om het toegangscontrolebeleid te formuleren. Voor elke toepassing wor dt dan een view connector gespecificeerd, die de access interface bindt aan de toepassing. Op basis van deze concepten, hebben we een toegangscontroledienst ontwik keld die een contextgebaseerd toegangsbeleid afdwingt met behulp van asp ectorientatie. Onze bevinding is dat de ondersteuning die aspectgeorient eerd software ontwikkeling (Aspect-Oriented Software Development (AOSD)) biedt om een doorsnijdend aspect te modulariseren, nuttig en nodig is v oor het modulariseren van het toegangscontroleaspect. Deze bevinding wor dt ondersteund door twee prototypes, die respectievelijk gebaseerd zijn op het AOSD-raamwerk JAC (Java Aspects Components) en de aspecttaal Caes arJ. Ten derde, werd ook een lijst opgesteld met evaluatiecriteria voor toega ngscontroletechnologieen en werd onze aanpak geevalueerd aan de hand van deze criteria. 1 Introduction 1.1 Access Control Challenges for Contemporary Distributed Applications 1.2 Separation of Concerns for Access Control Enforcement 1.3 Overview of the Chapters 2 Context-Based Access Control for Medical Applications 2.1 Introduction 2.2 Legislation 2.2.1 European Data Privacy Directive 2.2.2 US Health Insurance Portability and Accountability Act 2.3 Security Principles and Challenges for Health Care Systems 2.3.1 Organizational Measures 2.3.2 Technical Measures 2.3.3 Authorization 2.3.4 Principles addressed in this Thesis 2.4 A Representative Health Care Access Control Policy 2.5 Context-Based Access Control for Health Care 2.6 Conclusion 3 Evaluation of State-of-the-Art Access Control Technologies 3.1 Access Control Policies and Models 3.1.1 Access Control Policies 3.1.2 Access Control Management 3.1.3 Access Control Information 3.2 Access Control Architecture and Mechanism 3.2.1 Access Control Functions 3.2.2 Access Control Software Decomposition 3.2.3 Overview of an Access Control Enforcement Architecture 3.3 Evaluation Criteria for Access Control Technologies 3.3.1 Expressiveness 3.3.2 Evolution 3.3.3 Uniformity 3.4 State-of-the-Art Access Control Technologies 3.4.1 Java Authentication and Authorization Service 3.4.2 Java 2 Enterprise Edition 3.4.3 COM+ and .NET 3.4.4 CORBA Security Service 3.4.5 Tivoli Access Manager 3.4.6 Summary 3.5 Conclusion 4 Uniform Enforcement of Evolving Application-Domain-Specific Policies 4.1 Overview of the Approach 4.2 Access Interface 4.2.1 A Health Care-Specific Access Interface Example 4.2.2 Access Interface Syntax 4.2.3 Access Interface Semantics 4.3 View Connector 4.3.1 View Connector for a Health Care Application 4.3.2 View Connector Specification Syntax 4.3.3 View Connector Semantics 4.4 Discussion 4.4.1 Evaluation 4.4.2 Realization of the View Connector 4.4.3 Implementation Alternatives and Extensions 4.5 Conclusion 5 A Modular Access Control Service for Application-Domain-Specific Policies 5.1 Aspect-Oriented Software Development 5.2 Access Control Service Overview 5.3 Prototype Implementation in Java Aspect Components 5.3.1 Java Aspect Components 5.3.2 Design of the JAC Prototype 5.3.3 Discussion 5.4 Prototype Implementation in CaesarJ 5.4.1 CaesarJ 5.4.2 Pluggable Authentication Module Framework 5.4.3 Implementation of the Access Control Service 5.4.4 Discussion 5.5 Conclusion 6 Evaluation and Related Work 6.1 A Thorough Evaluation of the Access Control Service 6.1.1 Expressiveness 6.1.2 Policy Management 6.1.3 System Evolution 6.1.4 Scalability 6.1.5 Assurance 6.1.6 Conclusion 6.2 Applicability 6.3 Positioning in a Broader Perspective 6.3.1 Security Engineering 6.3.2 Policy Languages and Frameworks 6.3.3 AOSD and the Security Concern 6.3.4 Policy Enforcement Mechanisms 6.3.5 Context-Based Access Control 7 Conclusion 7.1 Contributions 7.2 Conclusion 7.3 Future Work Bibliography List of Publications Biography Dutch Summary nrpages: 144 + xxxiv status: published

Vele kritische computerprogramma's, met hoge betrouwbaarheidsvereisten, zijn gelijktijdig (m.a.w., de volgorde van de bewerkingen is niet volledig gespecificeerd) en zijn geschreven in op gedeeld geheugen gebaseerde gelijktijdige imperatieve programmeertalen. In de huidige stand van de technologie hebben programmeurs grote moeite met het afleveren van dergelijke programma's zonder programmeerfouten. Deze thesis stelt een aanpak voor die programmeurs kunnen gebruiken om te verifiëren dat een op gedeeld geheugen gebaseerd gelijktijdig imperatief programma, of een module van zo'n programma, vrij is van bepaalde vaak voorkomende programmeerfouten. Meer specifiek garandeert de aanpak de afwezigheid van dataraces en deadlocks en fouten tegen door de programmeur gespecificeerde correctheidscriteria. In deze aanpak annoteren programmeurs hun programma en voeren er dan een hulpprogramma op uit dat verificatiecondities genereert om te worden bewezen door een automatische stellingenbewijzer. De aanpak ondersteunt toestandsabstractie door middel van inspectormethodes, alsook onwijzigbare objecten en luie klasse-initialisatie. We hebben een prototype-implementatie ontwikkeld en met succes een aantal kleine programma's geverifieerd, en het verder werk nodig om de aanpak toepasbaar te maken in grote projecten geïdentificeerd. nrpages: 135 + vi status: published

Moderne softwaresystemen worden steeds frequenter opgebouwd als composities van herbruikbare componenten. Dergelijke componentgebaseerde software promoot vaak eenvoudige syntactische interfaces om het bouwen van nieuwe composities zo eenvoudig mogelijk te maken. Hoewel deze componenten op syntactisch niveau gemakkelijk samen te stellen zijn tot nieuwe composities, blijken losgekoppelde componenten echter regelmatig semantisch van elkaar af te hangen. Dit is onder andere het geval bij composities met een gemeenschappelijke opslagplaats (shared repository) via dewelke componenten indirect data met elkaar kunnen delen. Typisch worden deze verborgen afhankelijkheden niet gecontroleerd tijdens de compilatie, en op die manier leiden inbreuken op deze afhankelijkheden in huidige softwaresystemen tot fouten tijdens de uitvoering.De hoofdbijdrage van deze thesis is een aanpak om in toepassingen met een gemeenschappelijke opslagplaats het aantal fouten tijdens de uitvoering sterk te reduceren. We hebben uitgebreid ervaring opgedaan met dergelijke toepassingen in twee toepassingsdomeinen: componentgebaseerde protocolstapels en web toepassingen. Deze ervaringen illustreren duidelijk dat gebroken data afhankelijkheden in dergelijke applicaties een relevant probleem zijn en dat de fouten die eruit voorkomen een belangrijke impact kunnen hebben op de robuustheid en veiligheid van de toepassing. Onze aanpak baseert zich op de formele verificatie van de geen gebroken data afhankelijkheden compositie eigenschap. De formele verificatie van deze eigenschap wordt bereikt in twee stappen.In een eerste stap verifiëren we statisch dat een gegeven compositie met deterministische controle overgangen voldoet aan de gewenste compositie eigenschap. Hiertoe worden de componenten uitgebreid met contracten die de interacties met de gemeenschappelijke opslagplaats beschrijven in een probleemspecifieke contracttaal. Vervolgens volgen twee statische verificatiestappen. Eerst wordt nagegaan of het opgestelde component contract overeenkomt met de implementatie van de component. Ten slotte wordt de compositie eigenschap geverifieerd, steunend op de contracten van de verschillende componenten binnen de compositie.In een tweede stap breiden we de verificatie van de gewenste compositie eigenschap uit naar toepassingen met reactieve controle overgangen. Hierbij wordt de statische verificatie aanpak voor deterministische systemen gecombineerd met verificatie tijdens de uitvoering. Om de statische verificatie mogelijk te maken met de reactieve controle overgangen, definiëren we een bovengrens voor het reactieve gedrag. We noemen dit de vooropgestelde interacties tussen de web gebruiker en de toepassing, en drukken dit protocol uit in een gelabelde toestandsmachine.Daarna verifiëren we statisch of een gegeven compositie voldoet aan de compositie eigenschap, onder de veronderstelling dat elke interactie tussen de web gebruiker en de toepassing deel uitmaakt van de vooropgestelde interactie tussen de web gebruiker en de toepassing. We gebruiken hiervoor de oplossing voorgesteld voor deterministische controle overgangen. Ten slotte gebruiken we de protocolverificatie mogelijkheden van een Web Application Firewall om te garanderen dat enkel web aanvragen die deel uitmaken van de vooropgestelde interactie de web toepassing bereiken. Zo garanderen we dat de geen gebroken data afhankelijkheden compositie eigenschap geldt in een gegeven compositie.Ten slotte hebben we de formele verificatie van de geen gebroken data afhankelijkheden eigenschap gevalideerd in een toepassing met deterministische controle overgangen en een toepassing met reactieve controle overgangen. De statische verificatie uit de eerste stap werd succesvol toegepast op de webmail toepassing GatorMail. GatorMail is een middelgrote, open-source toepassing en bevat in totaal meer dan 1350 interacties met de gemeenschappelijke opslagplaats. Daarnaast werd de combinatie van statische en dynamische verificatie succesvol toegepast op de Duke's Bookstore e-commerce toepassing. In beide validatie experimenten werd een beperkte annotatie- en verificatiekost gemeten. Bovendien illustreerden beide experimenten dat de voorgestelde aanpak lineair schaalt naar grotere, realistische softwaretoepassingen, dankzij de modulaire specificatie en verificatie. 1 Introduction 1.1 Background 1.2 Problem Statement 1.3 Main Contributions 1.4 Overview of this Thesis 2 Indirect Data Sharing in Loosely-coupled Component Systems 2.1 Introduction 2.2 Indirect Data Sharing In Data-centered Applications 2.3 Case Study 1: Component-based Web Applications 2.3.1 Web Applications 2.3.2 A Servlet-based E-commerce Application 2.4 Case Study 2: Component-based Protocol Stacks 2.4.1 Protocol Stacks 2.4.2 DiPS+ Rapid Prototyping Infrastructure 2.4.3 A Simplified DiPS+ IPv4 Layer 2.4.4 Development of the DiPS+ Radius Layer 2.5 Goal and Scope of this Work 2.6 Related Work 2.7 Conclusion 3 Dependency Analysis of the GatorMail Webmail Application 3.1 Introduction 3.2 GatorMail 3.2.1 The Struts Framework 3.2.2 Composition Example 3.3 Dependency Analysis 3.3.1 Exploring Dependencies 3.3.2 Heuristic Identification of Dependencies 3.3.3 Abstract Application Model 3.4 Results 3.4.1 Overview of Dependencies 3.4.2 Key Characteristics 3.5 Conclusion 4 Static Verification of Indirect Data Sharing in Loosely-coupled Component Systems 4.1 Introduction 4.2 Background 4.2.1 Component Contracts and Static Verification 4.3 Problem Statement 4.3.1 Simplified Application Model 4.3.2 Composition Example 4.3.3 Desired Composition Properties 4.4 Solution 4.4.1 No Dangling Forwards Property 4.4.2 No Broken Data Dependencies Property 4.4.3 Unsoundness with ESC/Java2 4.5 Validation 4.5.1 Verifying Struts Applications: an Example 4.5.2 Results of the GatorMail Experiment 4.5.3 Discussion 4.6 Related Work 4.7 Conclusion 5 Bridging the Gap Between Web Application Firewalls and Web Applications 5.1 Introduction 5.2 Background 5.2.1 Web Vulnerabilities and Web Application Firewalls (WAFs) 5.3 Problem Statement 5.4 Solution 5.5 Prototype Implementation 5.5.1 Server-side Specification and Verification 5.5.2 Application-specific Protocol Verification 5.5.3 Run-time Protocol Enforcement 5.6 Discussion 5.6.1 Results of the BookStore Experiment 5.6.2 Limitations 5.7 Related Work 5.8 Conclusion 6 Conclusion 6.1 Summary 6.1.1 Main Contributions 6.1.2 Validation 6.2 Future Work 6.3 Developer-centric Verification 6.4 Concluding Thoughts nrpages: 119 + xxv status: published

When practicing secure programming, it is important to understand the restrictive influence programmed entities have on the propagation of authority in a program. To precisely model authority propagation in patterns of interacting entities, we present a new formalism Knowledge Behavior Models (KBM). To describe such patterns, we present a new domain specific declarative language SCOLL (Safe Collaboration Language), which semantics are expressed by means of KBMs. To calculate the solutions for the safety problems expressed in SCOLL, we have built SCOLLAR: a model checker and solver based on constraint logic programming. SCOLLAR not only indicates whether the safety requirements are guaranteed by the restricted behavior of the relied-upon entities, but also lists the different ways in which their behavior can be restricted to guarantee the safety properties without precluding their required functionality and (re-)usability. How the tool can help programmers to build reliable components that can safely interact with partially or completely untrusted components is shown in elaborate examples. (FSA 3)--UCL, 2007

Veilige software ontwikkelen blijft een uitdaging ondanks de kennis opgebouwd en tegenmaatregelen ontwikkeld in meer dan dertig jaar onderzoek naar computerbeveiliging. De resulterende onveiligheid manifesteert zich in een continue stroom van beveiligingszwakheden. Wanneer we deze beveiligingszwakheden aandachtig bestuderen, blijkt dat die meestal voorbeelden zijn van welgekende beveiligingsproblemen waarvoor tegenmaatregelen reeds geruime tijd voorhanden zijn. Waarom slagen softwareontwikkelaars er dan ondanks de bestaande tegenmaatregelen niet in de beveiligingszwakheden te voorkomen?Verschillende factoren, zoals marktgedreven softwareontwikkelingsplanning en gebrek aan beveiligingsbewustzijn, spelen hierin mee. Doorslaggevend is echter de beperkte economische aansporing voor softwareontwikkelaars om te investeren in softwarebeveiliging. Een probleem eigen aan de bestaande tegenmaatregelen is dat ze te duur geacht worden vanwege hun grote impact op de softwareontwikkelingsprocessen en de benodigde beveiligingsexpertise. In dit werk onderzoeken we de uitvoerbaarheid van pragmatische tegenmaatregelen die strikt los staan van het softwareontwikkelingsproces. We belichten voornamelijk tegenmaatregelen voor implementatie-gerelateerde beveiligingszwakheden in webtoepassingen.Dit onderzoek behelst drie delen, namelijk een studie van het probleemdomein, de ontwikkeling van een specifieke techniek voor het beveiligen tegen injectieaanvallen en de extensie van deze techniek naar het waarborgen van privacy.De studie van het probleemdomein heeft als doel het waarborgen van de relevantie van het te onderzoeken beveiliginsprobleem. Hiervoor hebben we een algemeen toepasbare methodologie ontwikkeld voor het taxonifiëren van beveiligingszwakheden op basis van de correlatie van de aanwezigheid van systeemeigenschappen en de toegeschreven invloed van deze eigenschappen op een selectie van historische beveiligingszwakheden. De toepassing van deze methodologie op Web Services heeft onthuld dat deze vatbaar zullen zijn voor beveiligingszwakheden gerelateerd aan de verificatie van invoer in het algemeen en injectiezwakheden in het bijzonder.Dit resultaat diende vervolgens als inbreng voor het tweede deel waarin we Context-Sensitive String Evaluation (CSSE), een vernieuwende en efficiënte maatregel tegen injectiezwakheden, ontwikkeld hebben. CSSE richt zich op de onderliggende oorzaak van injectiezwakheden, namelijk het vermengen van gegevens- en controlekanalen door ad hoc serialisatie. Door gebruik te maken van fijn-korrelige markering van veranderlijken, slaagt CSSE erin om volledig zelfstandig in een uit te voeren opdracht onderscheid te maken tussen de delen afkomstig van gebruikers (gegevens) en die afkomstig van ontwikkelaars (controle). Door vervolgens de delen afkomstig van gebruikers aan de noodzakelijke testen te onderwerpen, wordt het vermengen van beide kanalen vermeden.In het laatste deel hebben we CSSE uitgebreid met de functionaliteit nodig voor het waarborgen van privacy. Voorzieningen voor rijkere metadata, voor de bewaring van metadata en voor de beschrijving van het privacybeleid resulteerden in een praktische implementatie van het paradigma van het aangehechte privacybeleid. Op deze manier is het mogelijk om het consistent navolgen van de gegeven privacybeloftes doorheen de hele levenscyclus van persoonlijke informatie te waarborgen. Door gebruik te maken van het aspect-georiënteerde software ontwikkelingsparadigma zijn we erin geslaagd om de functionaliteit voor het waarborgen van privacy volledig te modulariseren en in te kapselen, wat het mogelijk maakt om het te gebruiken met bestaande toepassingen. nrpages: 141 status: published

When using mobile agents, numerous security issues must be considered. In this note we propose two methods to improve the security and reliability of mobile agent based transactions in an environment which may contain some malicious hosts.