Breaking Bits
  • What this gitbook is
  • Vulnerability Discovery
    • Reverse Engineering
      • Modern Vulnerability Research Techniques on Embedded Systems
      • Remote Dynamic Blackbox Java App Analysis
    • Emulation
      • QEMU Usermode Tracing
      • Building QEMU on Ubuntu
    • Fuzzing with AFL
    • Automated Vulnerability Discovery
      • Buffer Overflows
      • Analyzing Functions
    • Automatic Exploit Generation
      • Automatic Rop Chain Generation
  • CTF
  • Battelle Shmoocon 2024
    • Time Jump Planner
  • Spaceheros CTF 2022
    • RE: Shai-Hulud
  • UMDCTF 2020
    • UMDCTF 2020: Evil Santa's Mysterious Box of Treats
  • UMDCTF 2022
    • Tracestory
  • Spaceheroes CTF 2023
    • Everything-is-wrong
  • US CyberGames RE-Cruise 4
  • Firmware Emulator
  • Interactive Firmware Emulator Usage
  • Recreating CVE-2015-1187 in the DIR-820L
  • Exploit Development
    • Linux kernel exploit development
      • Setup
      • Interacting with Kernel Modules
      • Kernel stack cookies
      • Kernel Address Space Layout Randomization (KALSR)
      • Supervisor mode execution protection (SMEP)
      • Kernel page table isolation (KPTI)
      • Supervisor Mode Access Prevention (SMAP)
Powered by GitBook
On this page
  • Automatically detecting memory corruption
  • Understanding the memory corruption check
  • Piecing it together

Was this helpful?

  1. Vulnerability Discovery
  2. Automated Vulnerability Discovery

Buffer Overflows

Using angr to find overflows

PreviousAutomated Vulnerability DiscoveryNextAnalyzing Functions

Last updated 6 years ago

Was this helpful?

Automatically detecting memory corruption

is an awesome concolic analysis framework to recover control flow, solve CTF problems, and find bugs! The are a little old and pretty verbose. The interfaces provided by angr allow for much smaller scripts to do almost the exact same thing when detecting bugs.

The uses a pretty verbose stepping routine, where they step until they discover an unconstrained path resulting in a controllable program counter.

while exploitable_state is None:
    print(sm)
    sm.step()
    if len(sm.unconstrained) > 0:
        l.info("found some unconstrained states, checking exploitability")
        for u in sm.unconstrained:
            if fully_symbolic(u, u.regs.pc):
                exploitable_state = u
                break

I've found in my work, that the cost of asking if every bit inside of the program counter is symbolic slows down super large jobs. I've instead found that creating a method to query if a specific value is satisfiable runs much faster.

The code below will accept a simulation manager, check each unconstrained path to see if the program counter can point to "0x43434343"

def check_mem_corruption(simgr):
    if len(simgr.unconstrained):
        for path in simgr.unconstrained:
            if path.satisfiable(extra_constraints=[path.regs.pc == b"CCCC"]):
                path.add_constraints(path.regs.pc == b"CCCC")
                if path.satisfiable():
                    simgr.stashes['mem_corrupt'].append(path)
                simgr.stashes['unconstrained'].remove(path)
                simgr.drop(stash='active')
    return simgr

Understanding the memory corruption check

    if len(simgr.unconstrained):
        for path in simgr.unconstrained:

Unconstrained paths are program states where some form of symbolic data influences where the program instruction pointer points. When running bare bones projects from states like "blank states", data read from files, arguments passed to the programs, and any STDIN is often treated as symbolic data. The hope is that once some symbolic data corrupts the program counter, we check to see if it could result from any malicious user input.

            if path.satisfiable(extra_constraints=[path.regs.pc == b"CCCC"]):
                path.add_constraints(path.regs.pc == b"CCCC")
                if path.satisfiable():

Program state (or path) satisfiablility is asking the theorem prover (Microsoft's Z3) whether the current program state could exist given the current circumstances. The code above shows a constraint being imposed on the theorem prover to see if a program state could exist where the program counter can point to "0x43434343" (CCCC).

By using "CCCC" instead of the traditional "AAAA" on arm devices, when you analyze thumb mode code, PoCs generated produce "CCCB" for their program counter instead of "AAA@" when thumb mode rounds the last digit down.

Piecing it together

Building methods to determine vulnerability enables much more granulated specification of vulnerability types and the ability to stack multiple vulnerability checkers.

The code below uses a simulation manager checking function to determine vulnerability.

Overflow_Detector.py
import angr, argparse, IPython

def check_mem_corruption(simgr):
    if len(simgr.unconstrained):
        for path in simgr.unconstrained:
            if path.satisfiable(extra_constraints=[path.regs.pc == b"CCCC"]):
                path.add_constraints(path.regs.pc == b"CCCC")
                if path.satisfiable():
                    simgr.stashes['mem_corrupt'].append(path)
                simgr.stashes['unconstrained'].remove(path)
                simgr.drop(stash='active')
    return simgr

def main():
    parser = argparse.ArgumentParser()

    parser.add_argument("Binary")
    parser.add_argument("Start_Addr", type=int)

    args = parser.parse_args()

    p = angr.Project(args.Binary)
    state = p.factory.blank_state(addr=args.Start_Addr)
    
    simgr = p.factory.simgr(state, save_unconstrained=True)
    simgr.stashes['mem_corrupt']  = []
    
    simgr.explore(step_func=check_mem_corruption)

    IPython.embed()
    
if __name__ == "__main__":
    main()

angr
current write-ups
current method on the angr docs