Proof-Carrying Code: A Language-Based Security Approach Thao Doan Wei Hu Liqian Luo Jinlin Yang CS851 Malware 11/16/2004 Outline 1. 2. 3. 4. 5. 6. Introduction To Language-based Security Proof-carrying Code (PCC) Example 1: Network Packet Filters Example 2: A Certifying Compiler For Java Issues With PCC Discussion 11/16/2004 CS851 Malware 2 Part 1 Introduction to Language-Based Security 11/16/2004 CS851 Malware 3 Malicious code - A growing problem • What is malicious code? – “any code added, changed, removed from a software system in order to intentionally cause harm or subvert the intended function of the system.” • What makes it a growing problem? – Growing connectivity (the Internet) – Growing complexity of systems – Support for extensibility 11/16/2004 CS851 Malware 4 Two well-known security design principles • Principle of Least Privilege – a component should be given the minimum privilege necessary to accomplish its task – Ex: file access • Principle of Minimum Trusted Computing Base – keep the TCB as small and simple as possible (~ the KISS principle) – Ex: JVM, Proof Checker of PCC 11/16/2004 CS851 Malware 5 Approaches against malicious code • Analyze the code : before execution [reject] – Ex: scanning, compiler’s dataflow analysis • Rewrite the code : before execution [modify] – Ex: BEQZ R4, BadCode BEQZ R4, GoodCode • Monitor the code : during execution [stop before harm] – Ex: OS’ page translation hardware • Audit the code : during execution [police on harm] – Ex: audit trail to assess and address the problem 11/16/2004 CS851 Malware 6 Disadvantages of traditional approaches • • • • Miss unseen cases Trust entities required Performance Burden on consumers 11/16/2004 CS851 Malware 7 Motivation of language based security • Is it possible to enforce security on the semantics or behavior of the code? • Types, logics, & proofs come into play • Examples • Type-Safe Languages • Proof-Carrying Code 11/16/2004 CS851 Malware 8 Part 2 Proof-Carrying Code: Concept and Implementation 11/16/2004 CS851 Malware 9 Type-safe languages • Type – gives semantic meaning to ultimately mere bits – associated either with values in memory or with objects • Type-safe languages: – have complete type systems – e.g., Java, C#, ML • Code producer writes code in a type-safe language • Code consumer ensures code is safe: – static checks (e.g., type checks) – dynamic checks (e.g., array-bound checks) 11/16/2004 CS851 Malware 10 Cons of type-safe languages • Have large trusted computing base – many exploits of JVM itself has been reported http://www.cs.princeton.edu/sip/history/index.php3 • Require many run-time tests – casts, arrays, pointers, etc. • Incur inflexibility 11/16/2004 CS851 Malware 11 Proof-carrying code (PCC) Code Consumer Publicizes safety policy Code producer Provides Proof Native code Proof Validates Proof CPU 11/16/2004 [Necula, POPL’97] CS851 Malware 12 Benefits of PCC • Shifts the burden of ensuring the safety from code consumer to code producer • Can verify code in low-level languages • Fewer run-time checks Tamperproof Simpler, smaller, and faster TCB No cryptography or external authentication required 11/16/2004 CS851 Malware 13 Implementation of PCC • Proof generation theorem proving – extend first-order predicate logic to formalize the safety policy • Proof validation type checking – Edinburgh Logical Framework (LF) – map proof rules into types in LF 11/16/2004 CS851 Malware 14 PCC system architecture Code Consumer code in high level programming language Code Producer safety Policy compiler annotated assembly code Proof Generator 1. safety rules 2. module interface verification condition (VC) generator safety predicate 11/16/2004 validator theorem prover CS851 Malware proof native code 15 An example function on a DEC Alpha 11/16/2004 CS851 Malware 16 Part 3 Example 1 - Network Packet Filters [Necula et. al. OSDI'96] 11/16/2004 CS851 Malware 17 The problem • Examples – OS Extensions, Safe Mobile Code, Programming Language Interoperation • Previous Approaches – Hardware memory protection, Runtime checking, Interpretation • We want both safety and performance! 11/16/2004 CS851 Malware 18 The solution - PCC 11/16/2004 CS851 Malware 19 A PCC example • Goal – Test feasibility of PCC concept – Measure costs (proof size and validation time) – Choose simple but practical applications • Network Packet Filters 11/16/2004 CS851 Malware 20 Network packet filters user process space network monitoring application OS kernel packet filter network 11/16/2004 CS851 Malware 21 Safety policy 11/16/2004 CS851 Malware 22 Safety policy • Follow the BSD Packet Filter (BPF) model of safety – The packet is read-only. – The scratch memory is read-write. – No backward branches. – Only aligned memory accesses. 11/16/2004 CS851 Malware 23 Safety policy • Use first-order predicate logic extended with can_rd(addr) and can_wr(addr) • The precondition is: – – – – aligned memory addresses on an 8-byte boundary r0 (address of packet) r1 (length of packet) r2 (address of scratch memory (16 bytes)) 11/16/2004 CS851 Malware 24 Code certification 11/16/2004 CS851 Malware 25 Code certification • Step 1 - Compute a safety predicate for the code – for example: • For each LD r,n[rb] add can_rd(rb+n) • For each ST r,n[rb] add can_wr(rb+n) • Step 2 – Generate a proof (checkable) of the safety predicate 11/16/2004 CS851 Malware 26 Performance – experiment setup • 4 packet filters: – 1 Accepts IP packets (8 instr.) – 2 Accepts IP packets for 128.2.206 (15 instr.) – 3 IP or ARP between 128.2.206 and 128.2.209 (47 instr.) – 4 TCP/IP packets for FTP (28 instr.) • Compared with: – Interpretation: BSD Packet Filter – Runtime Checking: Software Fault Isolation – Type-safe Language: Modula-3 11/16/2004 CS851 Malware 27 Per-packet delay •PCC packet filters: fastest possible on the architecture •The point: Safety without sacrificing performance! 11/16/2004 CS851 Malware 28 Cost • Proofs are approx. 3 times larger than the code • Validation time: 0.3-1.8ms 11/16/2004 CS851 Malware 29 Startup cost amortization ms 15 12 9 6 3 0 PCC SFI M3 BPF 0 10 20 30 40 50 Thousands of packets • Conclusion: One-time validation cost amortized quickly 11/16/2004 CS851 Malware 30 Conclusion • A very promising framework for ensuring safety of untrusted code • Achieves safety without sacrificing performance • Serious difficulties exist • Needs more experiments 11/16/2004 CS851 Malware 31 Part 4 Example 2 - A certifying compiler for Java 11/16/2004 CS851 Malware 32 Certifying compiler (recap) [Colby et. al. PLDI ‘00] VC Generator Source Native Code Certifying Compiler Annotations VC Generator VC Axioms & Rules VC Proof Checker Proof Proof Generator Code Producer Code Consumer 11/16/2004 Axioms & Rules CS851 Malware 33 An example Class Poly{ Poly(float[] coefficients){…} float eval(float x){ float term = 1.0f; float result = 0.0f; for(int i=0; i<coefficients.length; i++){ result += coefficients[i] * term; term *= x; } return result; } private float[] coefficients; } 11/16/2004 CS851 Malware 34 for(int i=0; i<coefficients.length; i++){ result += coefficients[i] * term; term *= x; } LOOP_ENTRY: fxch %st(1) Register Value edx i eax coefficients ecx coefficients.length f6 term f7 result // result on top of FPU LOOP_INV = {(lt edx (sel4 rm (add eax 4))), (ge edx, 0), (type f7 jfloat), (type f6 jfloat)} flds 8(%eax, %edx, 4) // load coefficients[i] fmul %st(2), %st(0) // *term faddp fxch // +result %st(1) // term on top of FPU fmuls 12(%ebp) // *x incl %edx // i++ cmpl %ecx, %edx // i<coefficients.length? jl LOOP_ENTRY 11/16/2004 Loop Annotations // loop back if yes CS851 Malware 35 VC generation flds 8(%eax, %edx, 4) // load coefficients[i] prove: (saferd4 (add (sel4 rm_1 (add loc2_1 4)) It is safe to read coefficients[i] (add (imul edx_3 4) 8))) (rdArray4 (tyField (instFld A10 A32 A31) A30) A30 (sub0chk A34) szfloat (aidxi 4 (below1 (lt_b (geswap A38) A37)))) 11/16/2004 CS851 Malware 36 CC for modern OO languages Key Challenges: • Handle advanced language features – Dynamic creation of objects – Exception handling – Floating point arithmetic • Optimization • Cost (time & space) 11/16/2004 CS851 Malware 37 CC for Java • Handle dynamic object creation, exception handling, and float point arithmetic • Apply many standard optimizations • Proof size: 85% of the code size on average • Negligible checking time [Colby et. al. PLDI ‘00] 11/16/2004 CS851 Malware 38 Demo http://raw.cs.berkeley.edu/Ginseng/Images/p ccdemo.html 11/16/2004 CS851 Malware 39 Part 5 Issues with PCC 11/16/2004 CS851 Malware 40 Issues with PCC – Assuming: • • • • Trusted VCgen Trusted proof checker No bug in logical axioms No bug in typing rules – Type-specialized • built-in understanding of a particular type system 11/16/2004 CS851 Malware 41 Foundational PCC • Code provider provides: - executable code - proof in foundational logic • Eliminate implicit built-in logic Explicitly prove relevant concepts and their properties down to the foundation of mathematics 11/16/2004 CS851 Malware 42 Comparisons Type-specializedPCC Foundational PCC - Relies on VCgen - First-order logic - Built-in understanding of systems - No VCgen - Higher-order logic - Allows novel type system or safety arguments - Minimal proof checker (2700 LOC) - Large (~23000 LOC in Cedilla Systems) 11/16/2004 CS851 Malware 43 Foundational PCC • More secure • More flexible [Appel, LICS ’01] 11/16/2004 CS851 Malware 44 Discussion • What do you think is the hardest part in PCC implementation? • Which security problems doesn’t PCC address? • To what extent can it be applied? • Is it easy for legacy systems to adopt PCC? 11/16/2004 CS851 Malware 45
© Copyright 2024 ExpyDoc