Home

Basil Wiki

Welcome to the BASIL wiki!

What is BASIL?

BASIL generates semantically correct Boogie source files (.bpl) from AArch64/ARM64 binaries, with the intent of reasoning about concurrent programs through a rely-guarantee framework.

We use a lifter (currently BAP) to take a binary to an intermediate representation, BASIL's IR (IR). We then perform a series of conservative analyses on this to obtain an accurate representation of the program's structure. This is then translated into Boogie's IVL.

Wiki Contents

Developing

• Intellij
• VSCode

Program Structure

• ADT to BASIL IR translating
• BASIL IR
• Analyses

Misc

• .dot files for this Wiki