When will the TEMU component be released?

[simon]

TEMU component produces *.trace file which is translated to VINE
component.
In the example directory,there is only one file which is five.trace .
I want to test some my executable file , how can I get the .trace file?

[simon]

Or how does the .trace file construct? It is different from the .trace
file of JPF(Java Pathfinder), and I can open it with wordpad and
ultraedit, but they all show unreadable code.

[fisher_jiang]

The execution trace is the sequence of machine instructions executed,
and for each executed instruction, the value of
each operand, whether each operand is derived from the input, and if
it is derived from the input, an identifier for the
original input stream it comes from.

> > I want to test some my executable file , how can I get the .trace file?- 隐藏被引用文字 -
>
> - 显示引用的文字 -

[simon]

Yes,that should be the Taint Analysis Engine of TEMU.
Does TEMU take binary exection files as input,then produces a .trace
file?
If so, Rudder does the same thing,what is different?
Whether the Bitblaze System run like this:the Rudder deals with binary
exection file,then the result is the input to TEMU,and the VINE solves
all things?

> > - 显示引用的文字 -- 隐藏被引用文字 -
>
> - 显示引用的文字 -

[fisher_jiang]

As far as I know, Temu combined with Vine is kind of “Offline
Constraint Generation”.
The program is first traced by Temu and then appreplay models the
logic of the executed
instructions, generating a path constraint needed to force the
execution down the path.

On the contrary, Rudder is "Onine Constraint Generation" like EXE and
DART,
constraints are generated while the program is running, while Rudder
performing
mixed concrete and symbolic execution on binaries. The input to Rudder
is not
binary, Rudder's input comes from another component "Symbolic System
Environment",
which introduces symbolic inputs for any input source, e.g., a network
input, a file descriptor, libraries.
The Symbolic System Environment intercepts Windows API calls made by
the malicous software by adding hooks to QEMU's execution.

It seems bitblazers are not going to release Rudder :)

[simon]

Is there some source code written in C or C++ which performs symbolic
execution?
I know JPF SE performs symbolic execution,but it is written in JAVA
and orients only JAVA program

[fisher_jiang]

You may check GiNaC : http://www.ginac.de/

[simon]

Thanks a lot!

But is there some source code written in C or C++ which implements
binary analysis with symbolic execution as the Bitblaze system?

[Stephen McCamant]

>>>>> "S" == simon <ful...@gmail.com> writes:

S> TEMU component produces *.trace file which is translated to VINE
S> component. In the example directory,there is only one file which
S> is five.trace . I want to test some my executable file , how can I
S> get the .trace file?

As you suggest, the only way I know of to create files in BitBlaze's
.trace file format is using TEMU. We just made the TEMU release public
a few minutes ago; thanks for waiting.

S> Or how does the .trace file construct? It is different from the
S> .trace file of JPF(Java Pathfinder), and I can open it with wordpad
S> and ultraedit, but they all show unreadable code.

Yes, the .trace files are a binary format not shared with any
non-BitBlaze programs. The "trace_reader" utility included with Vine
can be used to print them in an ASCII format, and the Vine
distribution also includes OCaml libraries for reading the format.

S> Does TEMU take binary exection files as input,then produces a
S> .trace file?

TEMU is a whole-system emulator: in other words, it's a virtual
machine that you can run a whole operating system (Windows or Linux)
inside (somewhat like VMware or other virtual machines). While the
emulated system is running, you can give TEMU a command (using the
tracecap plugin) to record a trace of the instructions that a program
inside the emulator is running: that's where the .trace file comes
from.

S> If so, Rudder does the same thing,what is different?
S> Whether the Bitblaze System run like this:the Rudder deals with
S> binary exection file,then the result is the input to TEMU,and the
S> VINE solves all things?

Rudder represented a different approach to dynamic symbolic execution
("online", as opposed to "trace-based"). Rather than using a trace
file, the execution and the solving of symbolic formulas were
interleaved. So Rudder serves as an alternative to the process of
first generating a trace with TEMU and then processing it with Vine.
However, we have not released Rudder yet.

S> But is there some source code written in C or C++ which implements
S> binary analysis with symbolic execution as the Bitblaze system?

The parts of the BitBlaze system that implement dynamic symbolic
execution of binaries are split between TEMU and Vine, so some parts
of them are written in C and C++, but other parts are written in
OCaml. If you want a system that's entirely in C, you'll need to look
elsewhere. For instance you might want to look at SmartFuzz
(formerly "catchconv"):

http://www.sf.net/projects/catchconv

Hope this helps,

-- Stephen

[simon]

Thanks,It is very helpful!

On 11月24日, 上午6时35分, Stephen McCamant <s...@CS.Berkeley.EDU> wrote: