OPCDE/2017/Security Research and Development with LLVM - Andrew Reiter/projects.md

Security Related LLVM Projects

Some entries are on the cusp of security and non-security related. Please submit a pull request (or a friendly email) to add or remove projects. I highly doubt it is a complete list, so always welcoming additions and/or corrections. Further, I had thought to break out papers into it's own section, but decided against it for reasons related to sleep. And even further... There are some things I just wanted in here for informational reasons; i.e. they may not be projects. 🐫

Projects

AddressSanitizer (ASan)

Memory error detector for C/C++ finding UAF, buffer overflow, UAR, etc

GitHub Note the code in lib/Transform/Instrumentation.

``AddressSanitizer: A Fast Address Sanity Checker''

American Fuzzy Lop (AFL)

a security-oriented fuzzer that employs a novel type of compile-time instrumentation and genetic algorithms to automatically discover clean, interesting test cases that trigger new internal states in the targeted binary

http://lcamtuf.coredump.cx/afl

Andersen's Analysis

``Program Analysis and Specialization for the C Programming Language''

Standalone LLVM impl

ASAP (EPFL)

Analyze runtime checks to balance those that are needed and those that are not

http://dslab.epfl.ch/proj/asap/

Causal, Adaptive, Distributed, and Efficient Tracing System (CADETS)

address flaws in current audit and information-flow systems through fundamental improvements in dynamic instrumentation, scalable distributed tracing, and programming-language support.

http://www.cl.cam.ac.uk/research/security/cadets/

cclyzer

A tool for analyzing LLVM bitcode using Datalog.

GitHub

cspgen (Draper)

Map IR to models in Communicating Sequential Processes (CSP) process calculus.

GitHub

DangSan (VUSec)

Dangling pointer detection

GitHub

Paper

DataFlowSanitizer

Generalized data flow API

http://clang.llvm.org/docs/DataFlowSanitizerDesign.html

Divine

Explicit-state model checker

https://divine.fi.muni.cz

Thesis

DynamicTools

This project consists of several useful tool for dealing with LLVM IR runtime behaviors. Currently it consists of two parts, a custom-written LLVM IR interpreter, and an LLVM IR fuzzer (abandoned).

GitHub

fdc

An optimizing decompiler (for reversing)

http://zneak.github.io/fcd/

GitHub

FindFlows

https://llvm.org/svn/llvm-project/giri/trunk/lib/Static/FindFlows.cpp

Foreign Inference

Auto-generate wrappers for C code for Python etc.

GitHub Out of date, someone should revive and build LibFuzzer wrappers

Fracture (Draper)

Arch independent decompiler to LLVM IR (ver 3.6)

GitHub

Gist Static Analyzer (EPFL)

Failure-sketching to help determine reasons for faults

http://dslab.epfl.ch/proj/gist/

Paper

Trail of Bits CGC

``How we fared in the Cyber Grand Challenge''

Infer (Facebook)

Compile time static analyzer

http://fbinfer.com/

GitHub

Infer Clang Plugin

Kryptonite obfuscator

GitHub

KULFI (Utah)

Instruction level fault injector

GitHub

http://formalverification.cs.utah.edu/fmr/#kulfi

IKOS (NASA)

a C++ library designed to facilitate the development of sound static analyzers based on Abstract Interpretation

https://ti.arc.nasa.gov/opensource/ikos/

lafindel's transforms

Splitting certain compares to improve fuzzing

``Circumventing Fuzzing Roadblocks with Compiler Transformations''

LeakSanitizer

Memory leak detection

GitHub

LibFuzzer

Evolutionary, in-process guided fuzzing library

http://llvm.org/docs/LibFuzzer.html

GitHub

LibFuzzer Tutorial

llmc

``Model checking LLVM IR using LTSmin''

llStar

Pre/post condition intra-procedural verifier

https://bitbucket.org/jvillard/llstar/wiki/Home

Mc Sema (ToB)

Lift MC to IR for retargeting, patching, recompilation, symbolic exec

Github

MemorySanitizer

Detect pointer misalignment etc

GitHub and see source in lib/Transform/Instrumentation

Obfuscator-LLVM

GitHub

Note: https://github.com/obfuscator-llvm/obfuscator/tree/llvm-3.6.1/lib/Transforms/Obfuscation

Passes from QuarksLab

GitHub

``Turning regular code into atrocities''

Path Analysis for invariant Generation by Abstract Interpretation (PAGAI) (VERIMAG)

http://pagai.forge.imag.fr/

Also check out screen from trail of bits which makes use of PAGAI: https://github.com/trailofbits/screen

pmGen

Translate IR to Promela for verification

GitHub

PRESAGE (Utah)

protecting structured address computations against soft errors

http://formalverification.cs.utah.edu/fmr/#presage

[Git]https://utahfmr.github.io/PRESAGE/

Paper Basically, it attempts to reorganize GetElementPtr's to best handle alpha particle hits.

Pointer analysis with tunable precision (TPA)

GitHub

Remill (ToB)

Lift MC instructions to IR

GitHub

Return-less code

Transform IR to have no return statements.. attempt to avoid ROP

Paper

Rev.ng

Lift MC to IR by using QEMU

https://rev.ng/

Rev.ng LLVM developer mtg 2016

s2e (EPFL)

GitHub

SAFECode

http://safecode.cs.illinois.edu/

``Memory Safety for Low-Level Software/Hardware Interactions''

SafeInit (VUSec)

Detect uninitialized memory use errors

GitHub

Paper

Seahorn

Intraprocedural model checker

GitHub

See the links there to CRAB etc

Security-Oriented Analysis of Application Programs (SOAAP) (Cambridge)

http://www.cl.cam.ac.uk/research/security/ctsrd/soaap

GitHub

Sloopy

http://forsyte.at/people/pani/sloopy/

Smack

GitHub

http://soarlab.org/2014/05/smack-decoupling-source-language-details-from-verifier-implementations/

Software Analysis Workbench (SAW) (Galois Inc)

Formal verification via equivelancy checks

http://saw.galois.com/

GitHub SAW Script

GitHub llvm-verifier

Static Value Flow (SVF) (UNSW)

Pointer Analysis and Program Dependence Analysis for C and C++ Programs

http://unsw-corg.github.io/SVF/

GitHub

Temporally Enhanced Security Logic Assertions (TESLA) (Cambridge)

http://www.cl.cam.ac.uk/research/security/ctsrd/tesla

GitHub

TokenCap

Find tokens/magics in code so as to quickly pass fuzzing blockers

GitHub

Typesan (VUSec)

GitHub

Verified LLVM (VeLLVM)

Model syntax and semantics of LLVM IR in Coq for proving things about code reasoning on IR

http://www.cis.upenn.edu/~stevez/vellvm/

https://deepspec.org/main

Whole program LLVM

Help linking multiple .bc files to one

GitHub