Search

status: published

This paper describes the S3MS.NET run time monitor, a tool that can enforce security policies expressed in a variety of policy languages for .NET desktop or mobile applications. The tool consists of two major parts: a bytecode inliner that rewrites .NET assemblies to insert calls to a policy decision point, and a policy compiler that compiles source policies to executable policy decision points. The tool supports both singlethreaded and multithreaded applications, and is sufficiently mature to be used on real-world applications. This paper describes the overall functionality and architecture of the tool, discusses its strengths and weaknesses, and reports on our experience with using the tool on case studies as well as in teaching. ispartof: Electronic Notes in Theoretical Computer Science vol:253 issue:5 pages:153-159 ispartof: location:York 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

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

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