Uma entrevista interessante dms com o criador do MINIX, um dos primeiros projetos de microkernel com o espirito linux, Tovald se inspirou no minix pra criar o linux
pra quem nao sabe, minix foi desenvolvido pra estudos em OS e publicado pra estudo aberto, inclusive vc pode comprar ou baixar o livro que foi a base do desenvolvimento do MINIX, recomendo dms (Sistemas Operacionais: Projeto e Implementação)
Andrew Tannenbaum um dos primeiros gênios que acreditou e criou um dos primeiros ambientes colaborativos e livres, além de ser desenvolvido especificamente pra computadores com poucos recursos, sendo portável e potente

https://www.youtube.com/watch?v=OuRkUF1U8us

#angr #reverse #ctf #symbolicexecution

bem, estive pensando em escreve este post ha alguns dias, mas não sabia como começar ele. Então, vou dar uma resumida no começo caso seja do
seu interesse, você acompanha o post, se não, daqui a alguns dias postarei outras coisas
bem, antes de tudo, este post é sobre um assunto que pouco vi sendo falado na comunidade mas que é extremamente interessante e relevante

antes de começar seria interessante ter algum conhecimento prévio sobre testes de software e reversing (pelo menos as bases sobre posix e analise reverso)


execuçao simbolica: pra além da analise estatica

recentemente estava resolvendo alguns ctfs de engenharia reversa (voltada pra POSIX) e acabei me encontrando com um desafio que chamou bastante minha atençao, não vou entrar em muitos detalhes por enquanto, mas só vou dizer que ao fazer um analise abstrato (com radare2) acabei me encontrando com um main que parecia grande dms pra um challenge de nivel medio, sem muitas chamadas de functions

Ao analisar o main através de uma representação topológica (op:VV)
acabei me encontrando com uma estrutura interessantísima

representaçao em radare2 utilizando a sintaxe do ghidra (plugin r2ghidra)

bem, acabei não colocando aqui a representaçao topologica por uma questão de que no terminal do kali ficou bem estranho, pra fazer estes testes estou
utilizando kali linux-64bits, mas espero que tenha dado pra entender, no meu pessoal (debian(xfce4)) ficou melhor, mas pra isso existe cutter, um cliente gráfico pra radare2

um pequeno grafico que fiz a mão pra
explicar a topologia, desculpem se nao ficou mto bom mas vai dar pra entender

resumindo, o main pegava o input do user e fazia um teste comparativo (comparava a entrada do usuario como tamanho (hex0x20 = 32d) o qual deveria ter 32 strings

ateh ai tranquilo, mas o problema vinha mais a frente, já que dentro
destes testes condicionais haviam diferente operaçoes entre os values e no total eram feitos 31 testes condicionais e comparativos (31 ramificaçoes possiveis. lembre disso no futuro) , ou seja, em teoria teria que depurar 31 testes ateh encontrar cada string


Sinceiramente,isso levaria horas ou dias pra ser feito, já que teria que analisar a stack, os values de conversao e os testes comparativos atraves de breakpoints dentro de cada comparaçao

e foi ai que eu me perguntei, realmente não existe outra forma??
bem, dps desse pequeno desespero e já quase que me preparando pra dias de debugging acabei por procurar sobre algum noscript ou algum framework que me ajudasse
e ai meus users, acabei encontrando não apenas isso, senao um universo
novo, uma teoria conceitual completamente incrivel (pelo menos pra mim), ou como diriam os próprios desenvolvedores, magica

chegou a hora de conhecer Angr
ou melhor, a execuçao simbolica

execuçao simbolica: its magic??

tudo começo com estes post(https://blog.notso.pro/2019-03-20-angr-introduction-part0/) que acabei encontrando procurando sobre o assunto de grandes fluxos em testes de comparaçao

bem, mas como acontece??

imaginemos que temos um pedaço de code no qual ha um teste condicional (if,switch) e dentro deste teste temos um valor o qual desconhecemos mas que precissamos cumprir pra adentrar determinado fluxo de execuçao(literalmente o que vimos acima, porem neste caso utilizaremos apenas um teste comparativo em vez de 31). mas acontece que dentro deste teste comparativo vemos que determinado valor não esta explicito dentro da analise estatica, nem como uma string, nem como um valor, vemos ele apenas como uma aproximaçao que deve existir como resultado da execuçao ou de uma string que resulta do return de outra function

bem, o que é que a execuçao simbolica iria fazer??
neste caso (ha varias outras possibilidades mas irei falar delas mais a frente), a engine de execuçao simbolica (no nosso caso Angr) ira
simular o code e observar o fluxo (subarvore, ramificaçao,esturutra, nós) enfim, e analisara as condiçoes existentes e necessarias pra seguir as variantes, ou seja, o fluxo de execuçao em cada variante

outra forma mais curta de definir seria como uma execuçao abstrata na qual se toma em conta tdos os caminhos possíveis dentro do fluxo de execuçao (o input necessario pra execuçao é um simbolo já que não
possui um valor predefinido, dai a representaçao lambda, ou melhor, podemos criar ele como um vetor, uma string, uma string condicional de
inteiros, uma dword) enfim, é um simbolo pra execuçao das variante dentro do fluxo, lembrando que esta ocorre como uma simulaçao, ou seja, o code original nao é de fato executado, mas seu pedaço a ser simulado seria compartilhadopra a engine (Angr)

logo sua principal diferença com a execuçao abstrata, na qual tomamos em conta a estrutura geral do binario e não apenas um pedaço (o espaço onde ocorrem as comparaçoes e condicioanis) e todos estas variantes
são tomadas em conta, msm que representem um erro dentro do binario já que é um caminho possível a ser tomado

* um aviso importante é definir um ou vários caminhos a serem tomados já que em codes com multiplos caminhos e variantes (ou seja ramificaçoes dentro das condicionais) podemos ter uma explosao de caminhos, na qual a analise poderia levar bilhoes de anos (pensei nisso como uma taque de força bruta no qual precissa testar demasiadas
possibilidades), já que de fato o que Angr faz é estressar (ou seja, testar multiplas vezes como diferente possibilidades o value (simbolo) pra as
condicionais, um pouco parecido com um ataque de força bruta)

mas pra isso, nossos queridos devs do Angr (criado na universidade de santa barbara) nos permitem definir caminhos a serem evitados, a fim
de atingir o fluxo que definimos ou precissamos pra continuar a execuçao e neste caso, extrair a flag

extraindo as strings contidas no binario (do tipo elf, pie-enabled, ou seja, a cada execuçao o endereço de entrypoint se modifica) vemos que existe um endereço que pode nos apontar pra a flag, neste caso eh o 0x00002035 (license correct)

ao procurar por chamadas desse endereço dentro da main encontramos o endereço que resulta na flag (usando as referencias cruzadas do radare2 'axt @ 0x2035')

0x1876

agr o que nos resta eh usar Angr pra caminhar entre as ramificaçoes a fim de entrar nesse endereço e extrair a saida, evitando os endereços de erro, ou seja, os que resoltam em False

encontrando a flag através dos conceitos de execuçao simbolica

bem, tendo entendo isso, você deve estar se perguntando, como podemosurtilizar isto em ctfs??vamos lah, voltando pra o desafio do qual falei no começo

utilizando Angr

bem, sabendo que há uma forma de automatizar os testes de comparaçao
atraves de estresse do valor inserido, vamos procurar qual caminho devemos tomar pra encontrar a flag

baseado em aquelo outro grafico do main, vamos entender o que acontece dps de verificar que a string possui 32 bytes

aqui tento explicar a estrutura contida e o que precisa acontecer, como podemos ver, a ramificaçao false acaba entrando sempre no exit

tendo entendido, precissamos então utilizando (Angr) implementar uma execuçao simbolica que evite a entrada no exit e nos diga o resultado (lambda) que nos permite entrar em true dentro das ramificaçoes ateh atingir a flag

* execuçao simbolica atraves do fluxo de comparaçao
** evitar o caminho ateh o exit dentro desse pedaço de code
*** atingir o true
****receber o resultado de cada fluxo que atingirmos (as strings
comparadas que entrem em true)


implementado Angr e resolvendo o challenge

então, dps de entender o que precissamos fazer chegou a hora de implementar Angr
antes de tudo, precissamos chamar angr e claripy (claripy nos permite construir vetores abstratos dentro de python)

antes de inicializar, preciso definir o espaço do binario e chamo a funçao Project de Angr pra extrair o espaço da simulaçao e dou um argumento pra evitar o carregamento de librarys de chamada dentro do binario, já que tdo o code que precissamos simular esta dentro do binario


-
import angr
import claripy

espaço_challenge= “/home/user/challenge/challengebinary”

project = angr.Project(espaço_challenge, load_options={'auto_load_libs':False}


dps passamos a chamar claripy, o qual iremos dar o nome do nosso projeto como entrada pra criar um simbolo(que no angr sera nosso lambda) e passamos a chamar classe BVS pra definir como um vetor de bits que precissa ser de 32 bits (dado que é o input necessario pra o primeiro true)


argv = [project.filename]
size= 32
sym_arg= claripy.BVS('lambda-symbol', 8*size)
argv.append(sym_arg)


depois passamos alguns argumentos pra dizer a entrada da simulaçao e definimos algumas variaveis jah nosso challenge é um elf pie-enabled, o que acaba gerando conflitos durante a resoluçao de address (pra mais detalhes recomendo ver a documentaçao original, dentro da classe simulation)

entry_state= proj.factory.entry_state(args=argv,add_options={angr.sim_options.ZERO_FILL_UNCONSTRAINED_REGISTERS,angr.sim_options.ZERO_FILL_UNCONSTRAINED_MEMORY})

sim= project.factory.simulation_manager(entry_state)


damos os address no qual precissamos finalizar a simulaçao e o address que precissamos evitar(equivalente ao exit), nesse caso utilizo o address que vimos no radare2 + 0x4000 já que segundo a documentaçao de Angr é o address no qual Angr inicializa binarios com endereçamento aleatorio (PIE-Enabled)

exit_point = 0x400000+0x187d
avoid_point = 0x400000+0x1890

agr apenas resta iniciar a simulaçao, se vocês testarem num noscript podem acabar não percebendo mas se utilizarem a dle do python podem ver que nessa linha de codigo, o processo demora um pouco a retornar, é porque nesse momento que asimulaçao foi feita (de execuçao simbolica) e damos os argumentos dos address que precissamos encontrar e os que precissamos evitar, os quais foram as variaveis que acabamos de criar

tdo isso utilizando o modulo explore de simulaçao, recomendo ler na documentaçao pra entender mais detalhes e assim, implementando uma execuçao simbolica atraves de Angr, resta obter nossa flag e quando
angr encontrar o caminho relativo ao qual dizemos anteriormente(dentro do argumento) ele ira nos responder com um booleano (0:found, 1:not_found) e extraimoso value dentro do found


print (sim.found[0].solver.eval(argv[1], cast_to=bytes))

solver é uma classe contida em angr pra interagir com os vetores criados por claripy e extrair os valores em uma lista e dps usamos o argumento cast_to pra converter os values pra elementos legiveis (podem ser int ou qword)

e bem, é assim como acabei resolvendo mais um challenge e aprendendo um novo conceito interessantissimo,alem de conhecer um framework extremamente completo

agr alguns comentário, esse code é um pouco mais avançado mas se você procurar sobre o assunto pode acabar achando implementaçoes de Angr bem menos complexas , nesse caso eu fiz dessa forma pra resolver o challenge, mas recomendo dms resolver os challenges que o próprio Angr disponibiliza no seu repositorio pra começar a usar, talvez
fiquei mais tranquilo de entender



algumas referencias interessantes

https://docs.angr.io/ (docs de Angr)

Introduction to angr Part 0 (explicaçao da execuçao simbolica com alguns exemplos e resoluçoes dos challenge do Angr)

notes14-symbolic-execution.pdf (explicaçao detalha sobre execuçao simbolica)

PIE- Binary Exploitation (explicaçao de ofuscamento do PIE)

https://www.youtube.com/watch?v=BDKJf2kuwqg (um video bem legal do mente binaria no qual o rapaz acaba explicando sobre execuçao simbolica, não tem muito conteudo em si,mas recomendo dms os videos e o fórum do mente binaria)

foi muito utilizado o radare2 (plugin r2ghidra)

Bem, como votado por vcs, crie um novo canal, a primeira postagem sera feita aqui e pra seguir o conteudo do post eh soh entrar no canal, assim caso o topico seja do seu interesse, ficara melhor de ler e interagir
a primeira postagem sera sobre execuçao simbolica e adicionarei alguns detalhes sobre o que jah foi dito (testes de resoluçao baseados em satiasfibilidade)

dps vou postar um topico no qual irei me adentrar no mundo dos chips de monitoramento externo (intel ATM) e suas exploraçoes pela NSA, assim como uma documentaçao de como remover o firmware deste chip das nossas placas usando linux


https://news.1rj.ru/str/MoreRubyOfSec