jonathansalwan / triton Goto Github PK

movzx eax, byte ptr [rax] #22 = ((_ zero_extend 24) (_ bv97 8))
movsx eax, al             #23 = ((_ sign_extend 24) #22)
sub eax, 0x1              #24 = (bvsub #23 (_ bv1 32))
...
xor eax, 0x55             #31 = (bvxor #24 (_ bv85 32))
mov ecx, eax              #38 = #31
...
movzx eax, byte ptr [rax] #48 = ((_ zero_extend 24) (_ bv49 8))
movsx eax, al             #49 = ((_ sign_extend 24) #48)
cmp ecx, eax              #50 = (bvsub #38 #49)
                          ...
                          #56 = (assert (= #50 (_ bv0 32)))

L'extend sur le 23 n'est pas cencé avoir lieu car il y déjà l'extend au 22. Pareil pour 48 et 49.

Bonne formule :

(set-logic QF_AUFBV)
(declare-fun SymVar_0 () (_ BitVec 8))

(assert (= (bvsub (bvxor (bvsub ((_ sign_extend 24) ((_ zero_extend 0) SymVar_0)) (_ bv1 32)) (_ bv85 32)) ((_ sign_extend 24) ((_ zero_extend 0) (_ bv49 8)))) (_ bv0 32)))

(check-sat)
(get-model)
;(get-value (SymVar_1))

With:

• IDREF.CALLBACK.SYSCALL_ENTRY
• IDREF.CALLBACK.SYSCALL_EXIT

ADD :

Update compile.sh to a pin makefile

Currently, Triton applies an over approximation of the taint. Add sub-registers EAX, AX, AL, AH and spread the taint over these registers

• triton.getModel(expr)

0x4005d3        call 0x400450                           n/a
0x400450        jmp qword ptr [rip+0x200bc2]            n/a
0x400456        push 0x0                                #25 = (- #0 (_ bv8 64))
0x400456        push 0x0                                #26 = (_ bv0 64)
0x40045b        jmp 0x400440                            n/a
0x400440        push qword ptr [rip+0x200bc2]           n/a
0x400446        jmp qword ptr [rip+0x200bc4]            n/a
Don't display the trace if the current instruction is outside the .text like this call dans the PLT jump

Checkout :

• add
• mov
• cmp
• push
• pop

triton.startAnalysis(addr)
triton.endAnalysis(addr)
triton.rangeAnalysis(addr_start, addr_end)

• triton.setRegValue(IDREF.REG, value)

This trace viewer must parses the DB (#25)

We also need to restore the taint classe

Currently it exist a map address -> symvar but in some case we need the map symvar -> address.

Use something else than

• triton.getRegisterValue(IDREF.REG.RAX)

The point is to delete the dependence of the "pin.H" header in the "Register.h" header.
The goal is to have a Core totatlly free from any DBI framework's dependences.

One way to achieve this, it's to create maps between the DBI representation of registers and our inner
representation. These maps will be in pinContextHandler and each DBI specific contexthandler must implements
these kind of translation maps.

To reach a clean seperation between the DBI part and the Core part of Triton, I think it would be better
to always use our inner representation in the Core. For example, all IRBuilder classes must use ID_RBP and
not REG_RBP. So, I propose to systematically translate these IDs.
Also, in the pintool we should use the Pin API. This way there will be no doubt about which representation to use.

The direct inconvenient is that we will add some translation costs in function accessing the concrete context from our Core. However, a direct mapping in O(1) is not really a big cost for a cleaner design ;-).

The function derefMem is dangerous.

It try to dereference a pointer without knowing if it's valid or not ?

Example:

pin.sh -t triton.so -startAnalysis check -- samples/crackmes/crackme_sample

The crackme_sample try to read argv[1] even if there is no arguments at all and so it stops
abruptly with a segment fault.

However,right now, the SIGSEV signal comes from the pintool itself and not the program. That's
why our callback that would catch this signal doesn't work.
Sound fair, Pin instruments the program and not the pintool.
Here, the crash comes from the use of the derefMem function with a NULL pointer.

How can we handle this problem ?

This invalid dereferencement must happen, we seek this kind of crash!
The program must be the one doing it. So let's it doing first!

Solution:

- Each instruction where there is a dereferecement MUST be instrumented AFTER the execution
of the instruction!
- derefMem MUST be used only in callback called after the execution of the instruction!

Do something generic here

• triton.setMemValue(addr, writeSize, value)

The processingPyConf.callbackAfter() function must be called inside an INS_InsertCall() with the IPOINT_AFTER flag.

Example:

zfId = getRegSymbolicID(IDREF.FLAG.ZF)
expr = getBacktrackedSymExpr(zfId)
getModel(smt2lib.assert(smt2lib.equal(expr, smt2lib.bv(1, 1))))

triton.getMemValue(addr, size)

Check if it works on OSX

Maybe python bindings only for this interface.

OF with sub and add for example.

check: https://github.com/wisk/medusa/blob/dev/arch/x86.yaml#L44-54

Example:

#43 = (_ bv10 8)

• createSymVarFromID(43)

#43 = SymVar_4

Redesign of the class:

• the UINT64 symbolicReg[25] member should be private (no magic "25" constants also).
• the method newSymbolicElement()'s signature should change and accept a list of registers ID.
  Look at the example

Use inst::getThreadId() or PINContextHandler::getThreadId()

If a pintool works with the same outputs (stdout, stder) than the instrumented binary, all the informations displaying buy the tool is overwritten by the ouput of the binary.

We must do as the Pin's documentation says and write all the pintools ouputs in some others files.

So [dumpStat](https://github.com/JonathanSalwan/Triton/blob/master/src/bindings/python/callbacks.cpp#L78 should take a string in parameter) and dumpTrace.

Look at SymbolicEngine.h, we have two list playing the role of map. One is addresses to Reference ID and the other is addresses to Symbolic Variable ID.

So I suggest to change these lists to two maps (0(n) -> 0(log(n)).

Going to be useful when the DB will be generated.

• triton.getSymExprFromID(integer)
• triton.getFullSymExprFromID(integer)