Triton 에서의 테인트와 심볼릭에 관해

 

 

 

 

트리톤이 너무 빠르게 변하고 있어서..  수정은 개뿔 따라가기에도 정신이 없다.

트리톤에서 테인트 엔진이 왜 필요한지 모르겠는데 차라리 제거하는 것이 어떠냐는 질문에 조나단의 답이 아래와 같이 달렸다.

앞으로의 방향을 이해하기에 좋은 것 같음.

 

 

Taint analysis and symbolic execution are two different things. Inside Triton, taint analysis is useful for two main cases:

테인트와 심볼릭 두가지 다른점이 있다. 트리톤에서 테인트는 아래 두 가지를 위해서 유용하게 사용된다.

• First, when I open IDA, I like when I directly see what instructions are controlled by the user input. You can do that by generating a database with this tool and use a custom IDA plugin.

• 첫째. 아이다로 열때 input 값에 따라 어떤 인스트럭션이 taint 되었는지 바로 볼 수 있다. 커스텀 아이다플러그인이랑 generate_db.py 스크립트를 사용하면 됨.

• Then, the main objective of the taint engine inside Triton is to determine at each program point if we can ask a model to the solver. In fact, ask a model at each program point to know if we can influence the path condition or the register/memory value is really expensive. So, we only ask a model if we know that the instruction may be controllable by the user - it means that the symbolic expression contains symbolic variable(s). Otherwise, if the instruction is not tagged as tainted, it means that the symbolic expression can be replaced by a constant because nothing can influence the formula.

• 트리톤 테인트엔진의 주된 역할은, 프로그램의 특정 지점에서 solver 에게 모델을 질의할 수 있는지 아닌지를 판단하는 것이다. 사실 특정 시점에서 레지스터, 메모리 혹은 path condition 이 오염되었는지를 판단하는 것은 매우 많은 비용이 든다. 그래서 유저에 의해 contollable 할 수 있는 인스트럭션을 알고 있는 경우에만 - 심볼릭 익스프레션이 심볼릭 변수를 포함한다면- 질의를 한다.

 

 

 

Finally, in specific cases, we want to setup a symbolic variable without using the taint analyzer. So, that's why the symbolic engine and the taint engine are separated. In the long term, Triton will be a framework of program analysis not only a symbolic engine. So, we would like to separate all engines of each others.

결론적으로 테인트 엔진을 사용하지 않은 상태에서 심볼릭 변수를 세팅하는 것은 매우 특수한 경우다. 이것이 심볼릭 엔진과 테인트 엔진을 구분한 이유다. 트리톤은 심볼릭 엔진 뿐 아니라 프로그램 분석을 위한 프레임워크가 될 것이다.

So, how about removing taint and merge it to symboli execution engine? (like symbol.isTainted == True)

Actually, it's already (more or less) like that :)