search
Login | Signup | Support
  • 0
  • ×

    Add as FriendSoftware Control Flow Integrity

    by: Rogers

    Current Rating : Rate It :

    160

    Views

    Download
     
    1 : 1 Software Control Flow IntegrityTechniques, Proofs, & Security Applications Jay Ligatti summer 2004 intern work with: Úlfar Erlingsson and Martín Abadi
    2 : 2 Motivation I: Bad things happen DoS Weak authentication Insecure defaults Trojan horse Back door Particularly common: buffer overflows and machine-code injection attacks Source: http://www.us-cert.gov
    :
    :
    :
    6 : 6 Goal: Provably correct mechanisms that prevent powerful attackers from succeeding by protecting against all UCIT attacks Part of new project: Gleipnir This Research …in Norse mythology, is a magic chord used to bind the monstrous wolf Fenrir, thinner than a silken ribbon yet stronger than the strongest chains of steel. These chains were crafted for the Norse gods by the dwarves from “the sound of a cat's footfall and the woman's beard and the mountain's roots and the bear's sinews and the fish's breath and bird's spittle.”
    7 : 7 Attack Model Powerful Attacker: Can at any time arbitrarily overwrite any data memory and (most) registers Attacker cannot directly modify the PC Attacker cannot modify our reserved registers (in the handful of places where we need them) Few Assumptions: Data memory is Non-Executable * Code memory is Non-Writable * Also… currently limited to whole-program guarantees (still figuring out how to do dynamic loading of DLLs)
    :
    :
    10 : 10 Imprecise Return Information Q: What if FB can return to many functions ? Bret Acall+1 CFG excerpt Dcall+1 FB FA return call FB FD call FB succ(Bret) = {Acall+1, Dcall+1} A: Imprecise CFG
    11 : 11 No “Zig-Zag” Imprecision Acall B1 CFG excerpt C1 Ecall Solution I: Allow the imprecision
    12 : 12 Security Proof Outline Define machine code semantics Model a powerful attacker Define instrumentation algorithm Prove security theorem
    13 : 13 Security Proof I:Semantics (an extension of [HST+02]) “Normal” steps: Attack step: General steps:
    14 : 14 Security Proof II:Instrumentation Algorithm Insert new illegal instruction at the end of code memory For all computed jump destinations d with destination id X, insert “nop X” before d Change every jmp rs into: addi r0, rs, 0 ld r1, r0[0] movi r2, IMMX bgt r1, r2, HALT bgt r2, r1, HALT jmp r0 Where IMMX is the bit pattern that decodes into “nop X” s.t. X is the destination id of all targets of the jmp rs instruction.
    15 : 15 Security Proof III:Properties Instrumentation algorithm immediately leads to constraints on code memory, e.g.: Using such constraints + the semantics,
    16 : 16 SMAC Extensions In general, our CFG integrity property implies uncircumventable sandboxing (i.e., safety checks inserted by instrumentation before instruction X will always be executed before reaching X). Can remove NX data and NW code assumptions from language (can do SFI and more!): NW code addi r0, rd, 0 bgt r0, max(dom(MD)) - w, HALT bgt min(dom(MD)) - w, r0, HALT st r0(w), rs NX data addi r0, rs, 0 bgt r0, max(dom(MC)), HALT bgt min(dom(MC)), r0, HALT [checks from orig. algorithm] jmp r0
    17 : 17 Runtime Precision Increase Can use SMAC to increase precision Set up protected memory for dynamic information and query it before jumps E.g., returns from functions When A calls B, B should return to A not D Maintain return-address stack untouchable by original program
    18 : 18 Efficient Implementation ? Should be fast (make good use of caches): Checks & IDs same locality as code Static pressure on unified caches and top-level iCache Dynamic pressure on top-level dTLB and dCache How to do checks on x86 Can implement NOPs using x86 prefetching etc. Alternatively add 32-bit id and SKIP over it How to get CFG and how to instrument? Use magic of MSR Vulcan and PDB files
    19 : 19 Microbenchmarks Program calls pointer to “null function” repeatedly Preliminary x86 instrumentation sequences Normalized Overheads PIII = XP SP2, Safe Mode w/CMD, Mobile Pentium III, 1.2GHz P4 = XP SP2, Safe Mode w/CMD, Pentium 4, no HT, 2.4GHz
    20 : 20 Future Work Practical issues: Real-world implementation & testing Dynamically loaded code Partial instrumentation Formal work: Finish proof of security for extended instrumentation Proofs of transparency (semantic equivalence) of instrumented code Move to proof for x86 code
    21 : 21 References [CPM+98] Cowan, Pu, Maier, Walpole, Bakke, Beattie, Grier, Wagle, Zhang, Hinton. StackGuard: Automatic adaptive detection and prevention of buffer-overflow attacks. In Proc. of the 7th Unsenix Security Symposium, 1998. [HST+02] Hamid, Shao, Trifonov, Monnier, Ni. A Syntactic Approach to Foundational Proof-Carrying Code. Technical Report YALEU/DCS/TR-1224, Yale Univ., 2002. [XKI03] Xu, Kalbarczyk, Iyer. Transparent runtime randomization. In Proc. of the Symposium on Reliable and Distributed Systems, 2003.
    22 : 22 End

    Presentation Tags

    Copyright © 2019 www.slideworld.com. All rights reserved.