sushant94/rune

rune - radare2 based symbolic emulator

rune's Issues

Symbolic memory access

Add support for symbolic memory access in rune.

One simple way to solve this issue is to solve for the symbolic variable and spawn an instance of rune to work on each of these solutions.

Maximum depth for `DFSExplorer`

Cast operand widths

write implementation for RuneContext does not check if the size of destination and source are correct. This will lead to generation of invalid constraints which cannot be solved by the solver. A simple example where this can occus is in x86 instruction such as:
mov rax, ax

Add define_freevar to `Context`

Similar to define_const that is currently present but for defining symbolic variables

Path feasibilty

Check for path feasibility before dequeue to avoid taking impossible paths

Hooks and Breakpoints

Implement an API for hooks and breakpoints. Perhaps it is better to implement these as a part of esil-rs as other applications that use esil-rs will probably need some hooking functionality too.

Better integration with radare2

• Load breakpoints from flags in r2
• Load start address based on current seek in r2 (unless the start flag is set)
• Load register values set from r2.
• Raw commands to radare2

rune should use incremental solving features

From here. This will highly improve performance on repeated querying.

This would require feature additions and modifications in libsmt.rs.

Support `mem_write` for `write_size` != 64

Allow memory operations to accept u64 in addition to `VarRef`

• Use Into

Release checklist

• Point Cargo.toml to use non-local dependencies

Demo / Examples checklist

• Interactive explorer
• rune binary that parses command line options and sets up rune
• Interactive shell to query for constraints

Handle symbolic jumps

RuneContext currently cannot handle symbolic jumps. Some amount of refactoring is needed in order to implement this feature efficiently.

CI

• Setup Travis CI
• Setup coveralls

Basic repo tasks

• Add a README
• Add a LICENSE
• Logo

Engine semantics

• Formalize and document the Rune engine semantics. Currently, it seems a bit arcane and maybe missing all the needed functionality.
• Document and extend RuneControl functionality.
• Generalize Rune to accept instruction in any format (as opposed to the current limitation of LOpInfo).
• Generalize Rune to emit constraints in any form (as opposed to being restricted to QF_AUBV_Fn now).

readline in `runec::console::Console` to support history

Engine TODO List

• Handle Memory Read / Write
• Update esil vars

Add constraints for T/F branch in `BFSExplorer`

Scalability and radeco IL

Current implementation of context uses SMTLIB2 directly. This is not scalable on the long run as we do not perform any optimizations on the constraints that are generated before feeding it into the backend SMT solver.
This can be fixed by leveraging radeco IL from radeco IL and performing static analysis / optimizations before feeding the constraints to a solver.

As an added part of this task, concrete values must be treated differently from symbolic values. This reduces unnecessary constraints from being generated in the first place.

Easy creation of FileStream

Implement From<R2Stream> for FileStream in order to convert R2Stream into
a FileStream. This allows radare2 to be closed and additionally provides a
way to construct files that can be reused for further tests wihtout depending
on radare2.

Fix warnings

• Fix warnings in build
• Fix warnings after enabling rust_clippy to ensure better rust practices

Handle ExploreTrue and ExploreFalse differently in `rune::Rune`

Improve interactive explorer

• stash unexplored path options for future exploration

`Evaluate::eval` for `RuneContext` should check operand widths for compatibility

rune should allow users to set register values and start/break addresses in the console

Right now, the user requires to type in a long command to set up a session. This makes it a little cumbersome since a single error in the command would require them to fix the command again. It would be ideal if we could have a default context setup and then the user could interact in the console to set those values.

Example:

krypt0@chinmaydd: runec ./a.out
[+] Loading default context values
>> set zf=1
>> set break=0x8000
>> run
[+] Halted at 0x8000

Set esil_old / esil_new / lastsz based on assignments to registers

Set default widths of operands based on arch