Burt Triplett (burt@pbjtriplett.org)

Josh Triplett (josh@joshtriplett.org)

http://biosbits.org/

The Intel BIOS Implementation Test Suite (BITS) provides a bootable pre-OS environment for testing BIOSes and in particular their initialization of Intel processors, hardware, and technologies. BITS can verify your BIOS against many Intel recommendations. In addition, BITS includes Intel's official reference code as provided to BIOS, which you can use to override your BIOS's hardware initialization with a known-good configuration, and then boot an OS.

BITS supports scripting via Python, and includes Python APIs to access various low-level functionality of the hardware platform, including ACPI, CPU and chipset registers, PCI, and PCI Express. You can write scripts to explore and test platform functionality, using the full power of Python in 32-bit ring 0, without an OS in the way, and without recompiling BITS or writing custom C code.

???

Scripting Guide

https://bitbucket.org/cffi/profile/members

https://cffi.readthedocs.org

C Foreign Function Interface for Python. Interact with almost any C code from Python, based on C-like declarations that you can often copy-paste from header files or documentation.

???

???

Carl Pulley

https://bitbucket.org/carlpulley/libbap

BAP

Volatility/python interface to the Binary Analysis Platform (BAP) OCaml commands.

???

???

Jeff Forristal

https://code.google.com/p/lola-linux/

lola-linux

Linux kernel module to provide low level (hardware) access, for hardware research and driver prototyping purposes. Provides full memory access (physical DRAM + MMIO), IO, MSR, CPUID, and PCI config space.

???

???

Chema Garcia

https://github.com/sch3m4/pyadb

ADB

Simple python module to interact with the ADB tool

???

Example

zardus

https://github.com/zardus/pyvex

Valgrind

Python bindings for Valgrind's VEX IR.

Angr
rop_compiler

???

Sascha Böhme

http://www4.in.tum.de/~boehmes/z3-python.html

Z3

This is a Python binding to the SMT solver Z3. Since it is based on Python's dynamic foreign function interface ctypes, no compilation is required. Z3 is a high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research. These include: Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, SAGE, VS3, FORMULA, and HAVOC. It can read problems in SMT-LIB and Simplify formats.

???

site Z3