Falcon Intermediate Language.
Falcon IL is a simple, expression-based, well-defined, semantically-accurate intermediate language for the analysis of Binary Programs.
- Simple - Falcon IL has 21 expression types (including terminals), and 5 operation types, minimizing the work required to implement analyses.
- Expression-based - Falcon IL operates over expressions, as opposed to a three-address form like REIL/RREIL.
- Well-defined - Falcon IL is specified with rust's enumerated types, leaving no ambiguity in the IL.
- Semantically accurate - Falcon IL accurately captures the semantics of underlying architectures. This is mainly a function of the lifters. A divergence in the lifted semantics and the target architecture is a bug. This makes Falcon IL suitable for analyses which require precision in the semantics.
- Falcon IL does not support operations over values > 64 bits in width.
- Falcon IL does not support floating point operations.
While Falcon IL allows for analyses that find real bugs, due to these limitations it cannot completely analyze programs which require floating point or wide-register instructions.
You should think of components of the Falcon IL as belonging to two groups:
- Components which provide program semantics
- Components which provide location within a binary.
The following components provide semantics:
The following components provide location within a binary:
While this construct may seem verbose at first, in practice it is not. There are several convenience functions which allow for quickly gathering the necessary information from different components of the IL, and the IL is easily iterable.
The terminals in Falcon IL are
Constant is a valid, and Scalar is an identifier/variable.
Expressions implement basic arithemtic operations, comparison
operations, and bit extension/truncation operations over the terminals
Comparison expressions evaluate to a 1-bit expression with the value
True, and the value
It is an error to create an expresison which operates over expressions of
differing bitness. This is checked dynamically at runtime, and a
error wil be emitted if expressions have operands of differing bitness. It
is a bug if a lifter generates an expression with operands of differing
Trun should be used to ensure expressions
are of the same bitness.
Operation applies a transformation over some state. There are five
Operation in Falcon:
Assign: Assigns an
Store: Stores an
Expressionindexed by an
Expression. The size of the store will be determined by the size of the expression being stored.
Load: Loads an
Expressionindexed by an
Expression, and places the result into a
Scalar. The size of the load will be determined by the size of the Scalar being loaded into.
Branch: Branch to the address in the given
Raise: The raise operation takes a single
Expression, which is architecture/lifter-dependent, and allows for implementation of semantics which cannot be captured by Falcon IL, for example a system call.
When lifting, direct conditional branches such as X86
je or MIPS
not result in an
Operation::Branch. Instead, the instruction will be
omitted and edges will be emitted in the
ControlFlowGraph with expressions
which guard those edges.
Branch will only be emitted for indirect
Store are obviously dependent on the endianness of the target
architecture. Endianness is specified in the memory model, not in the IL.
An instruction provides position to an
Operation within a
also carries an optional
address. When an
Instruction is lifted from a
address field will be filled in.
You should not create an
Instruction explicitly, but instead call the
various methods over
Block corresponding to the
Operation you wish to
emit, and this will create the
Block is a basic block, or a sequence of
Block does not carry an
address field like
Instruction. Instead, a
Block has an
index field, which is an arbitray location within a
Edge connects two
Blocks in a
ControlFlowGraph. An edge has an
condition, which guards the edge. When direct conditional
branches are lifted from a program, this field will be filled in with the
condition that guards traversal of the edge.
We create a new
Edge by calling the
unconditional_edge methods on a
ControlFlowGraph is a directed graph with vertices of type
edges of type
A perhaps interesting property of
ControlFlowGraph is the
exit index. Falcon lifters lift individual
ControlFlowGraph, allowing them to capture semantics of
instructions which loop, such as X86's
repne scasb instruction.
Since all instructions have clearly defined entry and exit points, we can
use these to append their lifted graphs together. This is how Falcon's
lifters construct basic blocks.
A function holds an address, and a
ControlFlowGraph, applying location to
ControlFlowGraph. A function also has an optional
name, which will
be filled in by a
Loader when a corresponding symbol is available, as well
as an optional
index for when this function belongs to an
A program holds multiple instances of
Falcon IL may seem verbose, because of the many components, but in practice it is relatively simple and straight forward, with a minimal set of expressions and operations. Influenced by RREIL and Binary Ninja's IL, Falcon IL is my 3rd IL for binary program analysis, and strikes a good balance between simplicity and readability.
Unless writing a lifter, you should never have to create elements of the IL yourself, and can use the accessor methods to gather the information required.
A basic block in Falcon IL.
A constant value for Falcon IL
A directed graph of types
Edge between IL blocks
A function for Falcon IL. Provides location and context in a
An Instrinsic is a lifted instruction we cannot model.
A representation of a program by
A location independent of any specific instance of
A location applied to a
An IL Expression.
A location indepdent of any specific instance of
An IL Operation updates some state.
A location applied to a
A convenience function to create a new constant.
A convenience function to create a new constant expression.
A convenience function to create a new scalar expression.
A convenience function to create a new scalar.