Página Inicial>Código fonte JSP>Outras categorias
Baixar

Triton é uma biblioteca de análise binária dinâmica. Ele fornece componentes internos que permitem criar suas ferramentas de análise de programa, automatizar engenharia reversa, executar verificação de software ou apenas imitar o código.

  • Execução simbólica dinâmica
  • Análise de mancha dinâmica
  • Representação AST dos x86 , x86-64 , ARM32 , AARCH64 e RISC-V 32/64 ISA semântica
  • Síntese de expressões
  • A simplificação do SMT passa
  • Levantando para LLVM , bem como z3 e de volta
  • Interface SMT Solver para Z3 e Bitwuzla
  • API C ++ e Python


Como o Triton é uma espécie de projeto de meio período, não nos culpe se não for totalmente confiável. Problemas abertos ou solicitações de tração são sempre melhores que trolling =). No entanto, você pode seguir o desenvolvimento no Twitter @QB_TRITON.

Início rápido

  • Instalação
  • API Python
  • API C ++
  • Exemplos de Python
  • Eles já usaram Triton

Começando 

 from triton import *

> >> # Create the Triton context with a defined architecture
>> > ctx = TritonContext ( ARCH . X86_64 )

> >> # Define concrete values (optional)
>> > ctx . setConcreteRegisterValue ( ctx . registers . rip , 0x40000 )

> >> # Symbolize data (optional)
>> > ctx . symbolizeRegister ( ctx . registers . rax , 'my_rax' )

> >> # Execute instructions
>> > ctx . processing ( Instruction ( b" x48 x35 x34 x12 x00 x00 " )) # xor rax, 0x1234
> >> ctx . processing ( Instruction ( b" x48 x89 xc1 " )) # mov rcx, rax

> >> # Get the symbolic expression
>> > rcx_expr = ctx . getSymbolicRegister ( ctx . registers . rcx )
> >> print ( rcx_expr )
( define - fun ref ! 8 () ( _ BitVec 64 ) ref ! 1 ) ; MOV operation - 0x40006 : mov rcx , rax

>> > # Solve constraint
>> > ctx . getModel ( rcx_expr . getAst () == 0xdead )
{ 0 : my_rax : 64 = 0xcc99 }

>> > # 0xcc99 XOR 0x1234 is indeed equal to 0xdead
>> > hex ( 0xcc99 ^ 0x1234 )
'0xdead'

Instalar

Triton conta com as seguintes dependências: 

 * libcapstone                >= 5.0.x   https://github.com/capstone-engine/capstone
* libboost      (optional)   >= 1.68
* libpython     (optional)   >= 3.6
* libz3         (optional)   >= 4.6.0   https://github.com/Z3Prover/z3
* libbitwuzla   (optional)   >= 0.4.x   https://github.com/bitwuzla/bitwuzla
* llvm          (optional)   >= 12

Linux e MacOS 

$ git clone https://github.com/JonathanSalwan/Triton
$ cd Triton
$ mkdir build ; cd build
$ cmake ..
$ make -j3
$ sudo make install

Por padrão, LLVM e Bitwuzla não são compilados. Se você deseja aproveitar todo o poder de Triton, a compilação do CMake é: 

$ cmake -DLLVM_INTERFACE=ON -DCMAKE_PREFIX_PATH= $( llvm-config --prefix ) -DBITWUZLA_INTERFACE=ON ..

MacOS M1 Nota:

No caso de você receber erros de compilação como: 

 Could NOT find PythonLibs (missing: PYTHON_LIBRARIES PYTHON_INCLUDE_DIRS)

Tente especificar PYTHON_EXECUTABLE , PYTHON_LIBRARIES e PYTHON_INCLUDE_DIRS para sua versão específica do Python: 

 cmake -DCMAKE_INSTALL_PREFIX=/opt/homebrew/ 
      -DPYTHON_EXECUTABLE=/opt/homebrew/bin/python3 
      -DPYTHON_LIBRARIES=/opt/homebrew/Cellar/[email protected]/3.10.8/Frameworks/Python.framework/Versions/3.10/lib/libpython3.10.dylib 
      -DPYTHON_INCLUDE_DIRS=/opt/homebrew/opt/[email protected]/Frameworks/Python.framework/Versions/3.10/include/python3.10/ 
      ..

Esta informação você pode obter deste trecho: 

 from sysconfig import get_paths
info = get_paths ()
print ( info )

Windows

Você pode usar o cmake para gerar o arquivo .sln de libtriton. 

> git clone https://github.com/JonathanSalwan/Triton.git
> cd Triton
> mkdir build
> cd build
> cmake -G " Visual Studio 14 2015 Win64 " 
  -DBOOST_ROOT="C:/Users/jonathan/Works/Tools/boost_1_61_0" 
  -DPYTHON_INCLUDE_DIRS="C:/Python36/include" 
  -DPYTHON_LIBRARIES="C:/Python36/libs/python36.lib" 
  -DZ3_INCLUDE_DIRS="C:/Users/jonathan/Works/Tools/z3-4.6.0-x64-win/include" 
  -DZ3_LIBRARIES="C:/Users/jonathan/Works/Tools/z3-4.6.0-x64-win/bin/libz3.lib" 
  -DCAPSTONE_INCLUDE_DIRS="C:/Users/jonathan/Works/Tools/capstone-5.0.1-win64/include" 
  -DCAPSTONE_LIBRARIES="C:/Users/jonathan/Works/Tools/capstone-5.0.1-win64/capstone.lib" ..

No entanto, se você preferir fazer o download diretamente da biblioteca pré -compilada, consulte os artefatos do nosso aplicativo. Observe que, se você usar os artefatos do AppVeyor, provavelmente precisará instalar os pacotes redistribuíveis do Visual C ++ para o Visual Studio 2012.

Instalando a partir de vcpkg

O porto de Triton no VCPKG é mantido atualizado pelos membros da equipe da Microsoft e pelos colaboradores da comunidade. O URL do vcpkg é: https://github.com/microsoft/vcpkg. Você pode baixar e instalar o Triton usando o gerenciador de dependência vcpkg: 

$ git clone https://github.com/Microsoft/vcpkg.git
$ cd vcpkg
$ ./bootstrap-vcpkg.sh  # ./bootstrap-vcpkg.bat for Windows
$ ./vcpkg integrate install
$ ./vcpkg install triton

Se a versão estiver desatualizada, crie uma solicitação de problema ou puxe no repositório VCPKG.

Colaboradores

  • ALBERTO GARCIA ILELERA - Automação de cruzeiro
  • Alexey Vishnyakov - ISP Ras
  • Binário preto - n/a
  • Christian Heitman - Quarkslab
  • Daniil Kuts - ISP Ras
  • Jessy Campos - N/A
  • Matteo F. - N/A
  • Pierrick Brunet - Quarkslab
  • Pixelrick - n/a
  • Romain Thomas - Quarkslab
  • E muito mais

Eles já usaram Triton

Ferramentas

  • EXROP: geração automática de ropchain.
  • PIMP: plug -in R2 baseado em triton para execução concólica e controle total.
  • Ponce: vencedor do concurso de plug -in de IDA 2016! Execução simbólica a apenas um clique!
  • Qsynthesis: sintetizador de caixa cinza voltada para a deobfuscação de instruções de montagem.
  • Titondse: Biblioteca DSE baseada em Triton com recursos de carregamento e exploração.
  • Titan: Titan é um vmProtect DeVirtualizer usando o Triton.

Documentos e conferência

  • Syrd-Fuzz: Fuzzing Hybrid contínuo e análise dinâmica para o ciclo de vida do desenvolvimento de segurança
    Conferência em : Ivannikov ISP Ras Open Conference, Moscou, Rússia, 2022. [Paper] [Slide]
    Autores : Vishnyakov A., Kuts D., Logunova V., Parygina D., Kobrin E., Savidov G., Fedotov A.
    Resumo : Atualmente, as estruturas automatizadas de análise dinâmica para testes contínuos estão em alta demanda para garantir a segurança do software e satisfazer os requisitos do ciclo de vida de desenvolvimento de segurança (SDL). A eficiência de caça de insetos de segurança das técnicas de fuzzing híbrida de ponta supera a defesa guiada por cobertura amplamente utilizada. Propomos um pipeline de análise dinâmica aprimorada para alavancar a produtividade da detecção automatizada de bugs com base na fuzzing híbrida. Implementamos o pipeline proposto no Fuzz-Fuzz-Fuzz contínuo, que é alimentado pelo orquestrador híbrido de fuzzing, integrando nosso SYDR DSE Tool com Libfuzzer e AFL ++. O Sydr-Fuzz também incorpora verificadores predicados de segurança, CASR da ferramenta de triplo de falha e utilitários para minimização de corpus e coleta de cobertura. O benchmarking de nosso Fuzzher híbrido contra soluções alternativas de última geração demonstra sua superioridade sobre os fuzzhers guiados por cobertura, permanecendo no mesmo nível com fuzzhers híbridos avançados. Além disso, aprovamos a relevância de nossa abordagem, descobrindo 85 novas falhas de software no mundo real no projeto OSS-Sydr-Fuzz. Finalmente, abrimos o código fonte do CASR para a comunidade para facilitar o exame das falhas existentes.

  • Forte resolução otimista para execução simbólica dinâmica
    Conversa em : Ivannikov Memorial Workshop, Kazan, Rússia, 2022. [Paper] [Slide]
    Autores : Parygina D., Vishnyakov A., Fedotov A.
    Resumo : A execução simbólica dinâmica (DSE) é um método eficaz para testes automatizados do programa e detecção de bugs. Está aumentando a cobertura do código pela exploração complexa de ramificações durante a fuzz híbrida. As ferramentas DSE invertem as filiais ao longo de algum caminho de execução e ajudam o Fuzzher a examinar peças de programa anteriormente indisponíveis. O DSE costuma enfrentar problemas de excesso e subconstração. O primeiro leva a uma complicação significativa da análise, enquanto a segunda causa execução simbólica imprecisa. Propomos um forte método de resolução otimista que elimina restrições de predicado de caminho irrelevante para a inversão do ramo -alvo. Eliminamos essas restrições simbólicas das quais o ramo alvo não depende do controle. Além disso, lidamos separadamente ramificações simbólicas que aninham instruções de transferência de controle que passam pelo controle além do escopo da filial pai, por exemplo, retorno, goto, quebra etc. Implementamos o método proposto em nossa ferramenta de execução simbólica dinâmica SYDR. Avaliamos a forte estratégia otimista, a estratégia otimista que contém apenas a última negação de restrição e sua combinação. Os resultados mostram que a combinação de estratégias ajuda a aumentar a cobertura do código ou o número médio de filiais invertidas corretamente por um minuto. É ideal aplicar as duas estratégias em contraste com outras configurações.

  • Síntese do programa GreyBox: uma nova abordagem para atacar a ofuscação de fluxo de dados
    Fale em : Blackhat EUA, Las Vegas, Nevada, 2021. [Slide]
    Autores : Robin David
    Resumo : Esta palestra apresenta os últimos avanços na síntese de programas aplicados à deobfuscação. O objetivo é desmistificar essa técnica de análise, mostrando como ela pode ser colocada em ação na ofuscação. Especialmente a implementação qsynthesis divulgada para essa conversa mostra um fluxo de trabalho completo de ponta a ponta para desviar as instruções de montagem de volta às instruções otimizadas (deobfuscated) remontadas no binário.

  • Do código-fonte ao caso de teste de falha através da automação de testes de software
    Converse em : C & Esar, Rennes, França, 2021. [Paper] [Slide]
    Autores : Robin David, Jonathan Salwan, Justin Bourroux
    Resumo : Este artigo apresenta uma abordagem automatizando o processo de teste de software de um código -fonte para o teste dinâmico do programa compilado. Mais especificamente, a partir de um relatório de análise estática indicando alertas sobre as linhas de origem, ele permite que o teste cubra essas linhas dinamicamente e oportunisticamente, se eles podem ou não acionar uma falha. O resultado é um corpus de teste que permite cobrir alertas e desencadeá -los se eles forem verdadeiros positivos. Este artigo discute a metodologia empregada para rastrear alertas no binário binário compilado, no processo de seleção dos motores de teste e os resultados obtidos em uma implementação de pilha TCP/IP para sistemas incorporados e IoT.

  • Predicates de segurança simbólica: Hunt Program Frawyses
    Conferência em : Ivannikov ISP Ras Open Conference, Moscou, Rússia, 2021. [Paper] [Slide]
    Autores : A.Vishnyakov, V.Logunova, E.Kobrin, D.Kuts, D.Parygina, A.Fedotov
    Resumo : A execução simbólica dinâmica (DSE) é um método poderoso para exploração de caminhos durante fuzzing híbrido e detecção automática de bugs. Propomos predicados de segurança para detectar efetivamente o comportamento indefinido e os erros de violação de acesso à memória. Inicialmente, executamos simbolicamente o programa em caminhos que não acionam nenhum erro (a fuzz híbrida pode explorar esses caminhos). Em seguida, construímos um predicado de segurança simbólica para verificar alguma condição de erro. Assim, podemos alterar o fluxo de dados do programa para implicar a desreferência do ponteiro nulo, a divisão por zero, acesso fora dos limites ou fraquezas inteiras de transbordamento. Ao contrário da análise estática, a execução simbólica dinâmica não apenas relata erros, mas também gera novos dados de entrada para reproduzi -los. Além disso, introduzimos modelagem de semântica da função para funções comuns de biblioteca padrão C/C ++. Nosso objetivo é modelar o fluxo de controle dentro de uma função com uma única fórmula simbólica. Isso auxilia a detecção de bugs, acelera a exploração do caminho e supera o excesso de destaque no predicado do caminho. Implementamos as técnicas propostas em nossa ferramenta de execução simbólica dinâmica SYDR. Assim, utilizamos métodos poderosos de SYDR, como fatiamento de predicado de caminho que elimina restrições irrelevantes. Apresentamos a precisão da Juliet Dynamic para medir as ferramentas de detecção dinâmica de bugs. O sistema de teste também verifica que as entradas geradas acionam os desinfetantes. Avaliamos a precisão do SYDR para 11 CWEs do conjunto de testes de Julieta. SYDR mostra 95,59% de precisão geral. Dobramos os artefatos de avaliação SYDR disponíveis publicamente para facilitar a reprodutibilidade dos resultados.

  • Rumo ao raciocínio de ponteiros simbólicos em execução simbólica dinâmica
    Conversa em : Ivannikov Memorial Workshop, Nizhny Novgorod, Rússia, 2021. [Paper] [Slide]
    Autores : Daniil Kuts
    Resumo : A execução simbólica dinâmica é uma técnica amplamente usada para testes de software automatizados, projetados para a detecção de exploração e erros de programa de caminhos de execução. Uma abordagem híbrida se tornou generalizada, quando o principal objetivo da execução simbólica é ajudar a aumentar a cobertura do programa. Quanto mais ramificações executores simbólicos podem inverter, mais útil é para o Fuzzher. Um fluxo de controle de programa geralmente depende dos valores de memória, que são obtidos pela computação de índices de endereço da entrada do usuário. No entanto, a maioria das ferramentas DSE não suporta essas dependências, por isso perde algumas filiais de programas desejadas. Implementamos abordagens simbólicas O raciocínio nas leituras de memória em nossa ferramenta de execução simbólica dinâmica SYDR. As possíveis regiões de acesso à memória são determinadas analisando expressões simbólicas de endereço de memória ou pesquisa binária com SMT-Solver. Propomos uma técnica de linearização aprimorada para modelar acessos de memória. Diferentes métodos de modelagem de memória são comparados no conjunto de programas. Nossa avaliação mostra que o manuseio simbólico de endereços permite descobrir novas filiais simbólicas e aumentar a cobertura do programa.

  • Qsynth: uma abordagem baseada em síntese de programa para o código binário deobfuscation
    Converse em : Bar, San Diego, Califórnia, 2020. [Papel]
    Autores : Robin David, Luigi Coniglio, Mariano Ceccato
    Resumo : Apresentamos uma abordagem genérica que alavancava o DSE e a síntese de programas para sintetizar com sucesso programas ofuscados com a aritmética-aritmética-boolean, codificação ou virtualização de dados. O algoritmo de síntese proposto é uma síntese de enumeração offline primitiva, guiada pela pesquisa de deslocamento de cima para baixo. Mostramos sua eficácia contra um ofuscador de ponta e sua escalabilidade, pois substitui outras abordagens semelhantes baseadas na síntese. Também mostramos sua eficácia na presença de ofuscação composta (combinação de várias técnicas). Esse trabalho contínuo esclarece a eficácia da síntese para atingir certos tipos de ofuscações e abre caminho para algoritmos e estratégias de simplificação mais robustos.

  • SYDR: Execução simbólica dinâmica de ponta
    Conferência em : Ivannikov ISP Ras Open Conference, Moscou, Rússia, 2020. [Paper] [Slide] [Vídeo]
    Autores : A.Vishnyakov, A.Fedotov, D.Kuts, A.Novikov, D.Parygina, E.Kobrin, V.Logunova, P.Belecky, S.Kurmangaleev
    Resumo : A execução simbólica dinâmica (DSE) possui uma enorme quantidade de aplicações na segurança do computador (fuzzing, descoberta de vulnerabilidades, engenharia reversa, etc.). Propomos várias melhorias de desempenho e precisão para a execução simbólica dinâmica. O pular instruções não simbólicas permite construir um PATH Predicado 1,2-3,5 vezes mais rápido. O motor simbólico simplifica as fórmulas durante a execução simbólica. O fatiamento do predicado do caminho elimina conjuntos irrelevantes de consultas solucionadoras. Lidamos com cada tabela de salto (instrução Switch) como várias ramificações e descrevemos o método para a execução simbólica de programas com vários threads. As soluções propostas foram implementadas na ferramenta SYDR. SYDR realiza inversão de ramificações no predicado do caminho. O SYDR combina a ferramenta de instrumentação binária dinâmica do Dynamorio com o motor simbólico Triton.

  • Deobfuscation simbólica: do código virtualizado de volta ao original
    Fale em : Dimva, Paris-Saclay, França, 2018. [Paper] [Slide]
    Autores : Jonathan Salwan, Sébastien Bardin, Marie-Laure Ponet
    Resumo : A proteção de software ocupou um local importante durante a última década, a fim de proteger o software legítimo contra engenharia ou adulteração reversa. A virtualização é considerada uma das melhores defesas contra tais ataques. Apresentamos uma abordagem genérica baseada na exploração simbólica do caminho, mancha e recompilação, permitindo recuperar, de um código virtualizado, um código desviário semanticamente idêntico ao original e fechado em tamanho. Definimos critérios e métricas para avaliar a relevância dos resultados deobfuscados em termos de correção e precisão. Finalmente, propomos uma configuração de código aberto, permitindo avaliar a abordagem proposta em relação a várias formas de virtualização.

  • Deobfuscation de proteção de software baseada em VM
    Converse em : Sstic, Rennes, França, 2017. [Paper francês] [Slide inglês] [vídeo francês]
    Autores : Jonathan Salwan, Sébastien Bardin, Marie-Laure Ponet
    Resumo : Nesta apresentação, descrevemos uma abordagem que consiste em analisar automaticamente as proteções de software baseadas em máquinas virtuais e que recompila uma nova versão do binário sem essas proteções. Essa abordagem automatizada baseia -se em um guia de execução simbólica por uma análise de mancha e algumas políticas de concretização e, em seguida, em uma reescrita binária usando a transição de LLVM.

  • Como o Triton pode ajudar a reverter as proteções de software baseadas em máquina virtual
    Converse em : Csaw SOS, Nova York, Nova York, 2016. [Slide]
    Autores : Jonathan Salwan, Romain Thomas
    Resumo : A primeira parte da palestra será uma introdução à estrutura do Triton para expor seus componentes e explicar como eles trabalham juntos. Em seguida, a segunda parte incluirá demonstrações sobre como é possível reverter as proteções baseadas em máquinas virtuais usando análise de Taint, execução simbólica, simplificações SMT e otimizações de LLVM-IR.

  • Análise binária dinâmica e códigos ofuscados
    Converse em : St'hack, Bordeaux, França, 2016. [Slide]
    Autores : Jonathan Salwan, Romain Thomas
    Resumo : Nesta apresentação, falaremos sobre como um DBA (análise binária dinâmica) pode ajudar um engenheiro reverso a reverter o código ofuscado. Primeiro, introduziremos algumas técnicas básicas de ofuscação e depois exporemos como é possível quebrar algumas coisas (usando nossa estrutura de DBA de código aberto - Triton), como detectar predicados opacos, reconstruir CFG, encontrar o algoritmo original, isolar os dados sensíveis e muito mais ... então, concluiremos com um Demo e poucas palavras sobre os trabalhos futuros.

  • Como o Triton pode ajudar a analisar binários ofuscados
    Publicação em : Misc Magazine 82, 2015. [Artigo francês]
    Autores : Jonathan Salwan, Romain Thomas
    Resumo : A ofuscação binária é usada para proteger a propriedade intelectual do software. Existem diferentes tipos de obfutação, mas, aproximadamente, transforma uma estrutura binária em outra estrutura binária, preservando a mesma semântica. O objetivo da ofuscação é garantir que as informações originais sejam "afogadas" em informações inúteis que dificultam a engenharia reversa. Neste artigo, mostraremos como podemos analisar um programa obsceno e quebrar algumas ofuscações usando a estrutura Triton.

  • Triton: uma estrutura de execução concólica
    Conversa em : SSTIC, Rennes, França, 2015. [Paper francês] [Slide em inglês detalhado]
    Autores : Jonathan Salwan, Florent Saudel
    Resumo : Esta palestra é sobre o lançamento do Triton, uma estrutura de execução concólica baseada no PIN. Ele fornece componentes como um mecanismo de mancha, um mecanismo de execução simbólica dinâmica, um mecanismo de instantâneo, tradução da instrução x64 para SMT2, uma interface Z3 para resolver restrições e ligações de Python. Com base nesses componentes, o Triton oferece a possibilidade de criar ferramentas para pesquisa de vulnerabilidades ou assistência de engenharia reversa.

  • Análise de comportamento dinâmico usando instrumentação binária
    Converse em : St'hack, Bordeaux, França, 2015. [Slide]
    Autores : Jonathan Salwan
    Resumo : Esta palestra pode ser considerada como a parte 2 de nossa palestra no SecurityDay. Na parte anterior, conversamos sobre como era possível cobrir uma função direcionada na memória usando a abordagem DSE (Execução Simbólica Dinâmica). Cobrir uma função (ou seus estados) não significa encontrar todas as vulnerabilidades, alguma vulnerabilidade não trava o programa. É por isso que devemos implementar análises específicas para encontrar bugs específicos. Essas análises são baseadas na instrumentação binária e na análise de comportamento de tempo de execução do programa. Nesta palestra, veremos como é possível encontrar os seguintes tipos de bugs: Off-By-One, Stack / Heap Overflow, Use-After-Free, String de formato e {Write, Read} -Que-Where.

  • Cobrindo uma função usando uma abordagem de execução simbólica dinâmica
    Conversa em : Dia de Segurança, Lille, França, 2015. [Slide]
    Autores : Jonathan Salwan
    Resumo : Esta conversa é sobre análise e instrumentação binária. Veremos como é possível direcionar uma função específica, instantânea a memória/registro de contexto antes da função, traduzir a instrumentação em uma representação intermediária, aplicar uma análise de mancha com base nesse IR, construir/manter fórmulas para uma execução simbólica dinâmica até que a operação e a queda e a retração e a queda e a retração e a queda e a retração e a retração e a retração e a retração e a retração e a regra do que a operação e o regulamento e o regulamento e o regulamento e o retroções e o que o que é o que é o que é o que é o que é o que há para o que você está fazendo?

Cite Triton 

@inproceedings{SSTIC2015-Saudel-Salwan,
  author    = {Saudel, Florent and Salwan, Jonathan},
  title     = {Triton: A Dynamic Symbolic Execution Framework},
  booktitle = {Symposium sur la s{ ' {e}}curit{ ' {e}} des technologies de l'information
               et des communications},
  series    = {SSTIC},
  pages     = {31--54},
  address   = {Rennes, France},
  month     = jun,
  year      = {2015},
}
Expandir
Informações adicionais
Aplicativos Relacionados
Recomendado para você
Informações Relacionadas Todos