Inicio>código fuente JSP>Otras categorias
Descargar

Triton es una biblioteca de análisis binario dinámico. Proporciona componentes internos que le permiten construir sus herramientas de análisis de programas, automatizar la ingeniería inversa, realizar verificación de software o simplemente emular el código.

  • Ejecución simbólica dinámica
  • Análisis dinámico de mancha
  • Representación AST de la X86 , X86-64 , Arm32 , Aarch64 y Risc-V 32/64 Isa Semántica
  • Síntesis de expresiones
  • Pasa la simplificación SMT
  • Levantando a LLVM y a Z3 y atrás
  • Interfaz SMT Solver a Z3 y Bitwuzla
  • API C ++ y Python


Como Triton es una especie de proyecto a tiempo parcial, por favor, no nos culpe si no es completamente confiable. Los problemas abiertos o las solicitudes de extracción siempre son mejores que el trolling =). Sin embargo, puede seguir el desarrollo en Twitter @qb_triton.

Comienzo rápido

  • Instalación
  • API de Python
  • API C ++
  • Ejemplos de Python
  • Ya usaron Triton

Empezando 

 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 se basa en las siguientes dependencias: 

 * 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 y macOS 

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

Por defecto, LLVM y BitWuzla no se compilan. Si quieres disfrutar de toda la potencia de Triton, la compilación CMake es: 

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

Nota de MacOS M1:

En caso de que reciba errores de compilación como: 

 Could NOT find PythonLibs (missing: PYTHON_LIBRARIES PYTHON_INCLUDE_DIRS)

Intente especificar PYTHON_EXECUTABLE , PYTHON_LIBRARIES y PYTHON_INCLUDE_DIRS para su versión específica de 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 información que puede obtener de este fragmento: 

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

Windows

Puede usar CMake para generar el archivo .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" ..

Sin embargo, si prefiere descargar directamente la biblioteca precompilada, consulte los artefactos de nuestro Appveyor. Tenga en cuenta que si usa los artefactos de Appveyor, probablemente tenga que instalar los paquetes redistribuibles de Visual C ++ para Visual Studio 2012.

Instalación desde VCPKG

El puerto Triton en VCPKG se mantiene actualizado por los miembros del equipo de Microsoft y los contribuyentes comunitarios. La URL de VCPKG es: https://github.com/microsoft/vcpkg. Puede descargar e instalar Triton usando el Administrador de dependencias 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

Si la versión está desactualizada, cree un problema o extraiga la solicitud en el repositorio de VCPKG.

Colaboradores

  • Alberto García Illera - Automatización de cruceros
  • Alexey Vishnyakov - ISP Ras
  • Black Binary - 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
  • Y muchos más

Ya usaron Triton

Herramientas

  • Exrop: generación automática de Ropchain.
  • Pimp: complemento R2 basado en Triton para la ejecución concólica y el control total.
  • Ponce: ¡Ganador del concurso de complementos IDA 2016! Ejecución simbólica a solo un clic de distancia!
  • Qsynthesis: sintetizador Greybox orientado a la desobfuscación de las instrucciones de ensamblaje.
  • Tritondse: Biblioteca DSE basada en Triton con capacidades de carga y exploración.
  • Titan: Titan es un devirtualizer VMProtect usando Triton.

Documentos y conferencia

  • SYDR-Fuzz: Análisis dinámico y confuso híbrido continuo para el ciclo de vida del desarrollo de seguridad
    Hablar en : Ivannikov ISP Ras Open Conference, Moscú, Rusia, 2022. [Documento] [Diapositiva]
    Autores : Vishnyakov A., Kuts D., Logunova V., Parygina D., Kobrin E., Savidov G., Fedotov A.
    Resumen : Hoy en día, los marcos de análisis dinámico automatizado para pruebas continuas tienen una gran demanda para garantizar la seguridad del software y satisfacer los requisitos del ciclo de vida del desarrollo de seguridad (SDL). La eficiencia de caza de errores de seguridad de las técnicas de difusión híbrida de vanguardia superan a la difusión de cobertura ampliamente utilizada. Proponemos una tubería de análisis dinámico mejorado para aprovechar la productividad de la detección automatizada de errores basada en la difusión híbrida. Implementamos la tubería propuesta en el sydr-fuzz del conjunto de herramientas continuo que funciona con un orquestador difuso híbrido, integrando nuestra herramienta DSE SYDR con libfuzzer y AFL ++. Sydr-Fuzz también incorpora verificadores de predicados de seguridad, herramientas de triamiento de choque CASR y servicios públicos para minimización del corpus y recopilación de cobertura. La evaluación comparativa de nuestro fuzzador híbrido contra soluciones alternativas de estado de arte demuestra su superioridad sobre los fuzzers guiados por la cobertura y permanece en el mismo nivel con fuzzers híbridos avanzados. Además, aprobamos la relevancia de nuestro enfoque al descubrir 85 nuevas fallas de software del mundo real dentro del proyecto OSS-YDR-Fuzz. Finalmente, abrimos el código fuente CASR a la comunidad para facilitar el examen de los bloqueos existentes.

  • Fuerte resolución optimista para la ejecución simbólica dinámica
    Hablar en : Ivannikov Memorial Workshop, Kazan, Rusia, 2022. [Documento] [Diapositiva]
    Autores : Parygina D., Vishnyakov A., Fedotov A.
    Resumen : La ejecución simbólica dinámica (DSE) es un método efectivo para las pruebas y detección de errores automatizadas del programa. Está aumentando la cobertura del código por la compleja exploración de ramas durante la lucha híbrida. Las herramientas DSE invierten las ramas a lo largo de algunas rutas de ejecución y ayudan a los fuzzadores a examinar las piezas del programa no disponibles previamente. DSE a menudo enfrenta problemas de restricción excesiva y deprimente. El primero conduce a una complicación de análisis significativa, mientras que el segundo causa una ejecución simbólica inexacta. Proponemos un método de resolución optimista fuerte que elimina las restricciones de predicado de ruta irrelevante para la inversión de la rama objetivo. Eliminamos tales restricciones simbólicas en las que la rama objetivo no depende del control. Además, manejamos por separado las ramas simbólicas que tienen instrucciones de transferencia de control anidadas que pasan el control más allá del alcance de la rama principal, por ejemplo, retorno, GoTo, Break, etc. Implementamos el método propuesto en nuestra herramienta dinámica de ejecución simbólica SYDR. Evaluamos la fuerte estrategia optimista, la estrategia optimista que contiene solo la última negación de restricciones y su combinación. Los resultados muestran que la combinación de estrategias ayuda a aumentar la cobertura del código o el número promedio de ramas correctamente invertidas por un minuto. Es óptimo aplicar ambas estrategias juntas en contraste con otras configuraciones.

  • Síntesis del programa GreyBox: un nuevo enfoque para atacar la ofuscación del flujo de datos
    Hablar en : Blackhat USA, Las Vegas, Nevada, 2021. [Diapositiva]
    Autores : Robin David
    Resumen : Esta charla presenta los últimos avances en la síntesis del programa aplicado para la deobfuscación. Su objetivo es desmitificar esta técnica de análisis mostrando cómo se puede poner en acción sobre la ofuscación. Especialmente la implementación Qsynthesis publicada para este programa de entrevistas Un flujo de trabajo completo de extremo a extremo para desobfuscar las instrucciones de ensamblaje en las instrucciones optimizadas (desobfuscadas) se volvieron a montar en el binario.

  • Desde el código fuente hasta el caso de prueba de bloqueo a través de la automatización de pruebas de software
    Hablar en : C & Esar, Rennes, Francia, 2021. [Documento] [Diapositiva]
    Autores : Robin David, Jonathan Salwan, Justin Bourroux
    Resumen : Este documento presenta un enfoque que automatiza el proceso de prueba de software desde un código fuente hasta la prueba dinámica del programa compilado. Más específicamente, a partir de un informe de análisis estático que indica alertas en las líneas de origen, permite que las pruebas cubran estas líneas controlando dinámica y de manera oportunista si pueden o no activar un bloqueo. El resultado es un corpus de prueba que permite cubrir alertas y activarlas si son verdaderos positivos. Este artículo discute la metodología empleada para rastrear alertas en el binario compilado, el proceso de selección de motores de prueba y los resultados obtenidos en una implementación de la pila TCP/IP para sistemas integrados e IoT.

  • Predicados de seguridad simbólicos: debilidades del programa de caza
    Hablar en : Ivannikov ISP Ras Open Conference, Moscú, Rusia, 2021. [Documento] [Diapositiva]
    Autores : A.Vishnyakov, V.Logunva, E.Kobrin, D.Kuts, D.Parygina, A. Fedotov
    Resumen : La ejecución simbólica dinámica (DSE) es un método poderoso para la exploración de rutas durante la detección de errores híbridos y de error híbrido. Proponemos predicados de seguridad para detectar efectivamente el comportamiento indefinido y los errores de violación de acceso a la memoria. Inicialmente, ejecutamos simbólicamente el programa en rutas que no desencadenan ningún error (la confusión híbrida puede explorar estas rutas). Luego construimos un predicado de seguridad simbólico para verificar alguna condición de error. Por lo tanto, podemos cambiar el flujo de datos del programa para implicar la deserferencia de puntero nulo, división por cero, acceso fuera de los límites o debilidades de desbordamiento entero. A diferencia del análisis estático, la ejecución simbólica dinámica no solo informa errores, sino que también genera nuevos datos de entrada para reproducirlos. Además, introducimos modelado semántico de funciones para funciones comunes de biblioteca estándar C/C ++. Nuestro objetivo es modelar el flujo de control dentro de una función con una sola fórmula simbólica. Esto ayuda a la detección de errores, acelera la exploración de la ruta y supera las sobreconstramentos en el predicado de ruta. Implementamos las técnicas propuestas en nuestra herramienta de ejecución simbólica dinámica Sydr. Por lo tanto, utilizamos métodos poderosos de SYDR, como el corte de predicado de ruta, que elimina las restricciones irrelevantes. Presentamos a Juliet Dynamic para medir la precisión de las herramientas de detección de errores dinámicos. El sistema de prueba también verifica que las entradas generan desencadenantes desencadenantes. Evaluamos la precisión de SYDR para 11 CWE de Juliet Test Suite. SYDR muestra el 95.59% de precisión general. Hacemos que los artefactos de evaluación SYDR estén disponibles públicamente para facilitar la reproducibilidad de resultados.

  • Hacia el razonamiento simbólico de punteros en la ejecución simbólica dinámica
    Hablar en : Ivannikov Memorial Workshop, Nizhny Novgorod, Rusia, 2021. [Documento] [Diapositiva]
    Autores : Daniil Kuts
    Resumen : La ejecución simbólica dinámica es una técnica ampliamente utilizada para pruebas de software automatizadas, diseñada para la exploración de rutas de ejecución y la detección de errores del programa. Un enfoque híbrido se ha generalizado recientemente, cuando el objetivo principal de la ejecución simbólica es ayudar a aumentar la cobertura del programa. Cuantas más ramas puedan invertir el ejecutor simbólico, más útil es para el fuzzer. Un flujo de control del programa a menudo depende de los valores de memoria, que se obtienen mediante índices de dirección informática de la entrada del usuario. Sin embargo, la mayoría de las herramientas DSE no admiten tales dependencias, por lo que pierden algunas ramas de programas deseadas. Implementamos direcciones simbólicas razonamiento en lecturas de memoria en nuestra herramienta dinámica de ejecución simbólica SYDR. Las posibles regiones de acceso a la memoria se determinan analizando expresiones simbólicas de la dirección de memoria o la búsqueda binaria con SMT-Sanguls. Proponemos una técnica de linealización mejorada para modelar los accesos de memoria. Se comparan diferentes métodos de modelado de memoria en el conjunto de programas. Nuestra evaluación muestra que el manejo de las direcciones simbólicas permite descubrir nuevas ramas simbólicas y aumentar la cobertura del programa.

  • Qsynth: un enfoque basado en síntesis de programa para el código binario deobfuscation
    Hablar en : Bar, San Diego, California, 2020. [Documento]
    Autores : Robin David, Luigi Coniglio, Mariano Ceccato
    Resumen : Presentamos un enfoque genérico que aprovecha la síntesis de DSE y del programa para sintetizar con éxito programas ofuscados con aritmética booleana mixta, codificación de datos o virtualización. El algoritmo de síntesis propuesto es una síntesis enumerada fuera de línea primitiva guiada por la búsqueda de respiración de arriba hacia abajo. Mostramos su efectividad contra un ofuscador de última generación y su escalabilidad, ya que reemplaza otros enfoques similares basados ​​en la síntesis. También mostramos su efectividad en presencia de ofuscación compuesta (combinación de varias técnicas). Este trabajo continuo ilumina la efectividad de la síntesis para dirigirse a ciertos tipos de ofuscaciones y abre el camino a algoritmos más sólidos y estrategias de simplificación.

  • SYDR: Ejecución simbólica dinámica de vanguardia
    Hablar en : Ivannikov ISP Ras Open Conference, Moscú, Rusia, 2020. [Documento] [Diapositiva] [Video]
    Autores : A.Vishnyakov, A.Fedotov, D.Kuts, A.Novikov, D.Parygina, E.Kobrin, V.Logunva, P.Belecky, S.KurmangaleEV
    Resumen : La ejecución simbólica dinámica (DSE) tiene una enorme cantidad de aplicaciones en seguridad informática (confuso, descubrimiento de vulnerabilidad, ingeniería inversa, etc.). Proponemos varias mejoras de rendimiento y precisión para la ejecución simbólica dinámica. Saltar instrucciones no simbólicas permite construir un predicado de ruta 1.2-3.5 veces más rápido. El motor simbólico simplifica las fórmulas durante la ejecución simbólica. El corte de predicado de ruta elimina los conjuntos irrelevantes de las consultas del solucionador. Manejamos cada tabla de salto (instrucción Switch) como múltiples ramas y describimos el método para la ejecución simbólica de programas de múltiples subprocesos. Las soluciones propuestas se implementaron en la herramienta SYDR. SYDR realiza la inversión de ramas en el predicado de ruta. SYDR combina la herramienta de instrumentación binaria dinámica Dynamorio con el motor simbólico Triton.

  • Deobfuscación simbólica: desde el código virtualizado de regreso al original
    Hablar en : Dimva, Paris-Saclay, Francia, 2018. [Documento] [Diapositiva]
    Autores : Jonathan Salwan, Sébastien Bardin, Marie-Laure Potet
    Resumen : La protección del software ha tomado un lugar importante durante la última década para proteger el software legítimo contra la ingeniería inversa o la manipulación. La virtualización se considera una de las mejores defensas contra tales ataques. Presentamos un enfoque genérico basado en la exploración de rutas simbólicas, la mancha y la recompilación que permite recuperarse, de un código virtualizado, un código devirtualizado semánticamente idéntico al original y de tamaño cercano. Definimos criterios y métricas para evaluar la relevancia de los resultados desobfuscados en términos de corrección y precisión. Finalmente, proponemos una configuración de código abierto que permite evaluar el enfoque propuesto contra varias formas de virtualización.

  • Desobfuscación de protección de software basada en VM
    Hablar en : SSTIC, Rennes, Francia, 2017. [Papel francés] [Diapositiva en inglés] [Video francés]
    Autores : Jonathan Salwan, Sébastien Bardin, Marie-Laure Potet
    Resumen : En esta presentación describimos un enfoque que consiste en analizar automáticamente las protecciones de software basadas en máquinas virtuales y que recompensa una nueva versión del binario sin tales protecciones. Este enfoque automatizado se basa en una guía de ejecución simbólica mediante un análisis de contaminación y algunas políticas de concretización, luego en una reescritura binaria utilizando la transición LLVM.

  • Cómo Triton puede ayudar a revertir las protecciones de software basadas en máquinas virtuales
    Hablar en : CSAW SOS, NYC, Nueva York, 2016. [Diapositiva]
    Autores : Jonathan Salwan, Romain Thomas
    Resumen : La primera parte de la charla será una introducción al marco de Triton para exponer sus componentes y explicar cómo trabajan juntos. Luego, la segunda parte incluirá demostraciones sobre cómo es posible revertir las protecciones basadas en máquinas virtuales utilizando el análisis Taint, la ejecución simbólica, las simplificaciones SMT y las optimizaciones LLVM-IR.

  • Análisis binario dinámico y códigos ofuscados
    Hablar en : St'hack, Burdeos, Francia, 2016. [Diapositiva]
    Autores : Jonathan Salwan, Romain Thomas
    Resumen : En esta presentación hablaremos sobre cómo un DBA (análisis binario dinámico) puede ayudar a un ingeniero inverso a un código ofuscado inverso. Primero introduciremos algunas técnicas básicas de ofuscación y luego expondremos cómo es posible romper algunas cosas (usando nuestro marco DBA de código abierto - Triton) como detectar predicados opacos, reconstruir CFG, encontrar el algoritmo original, aislar datos sensibles y muchos más ... luego, concluiremos con una demostración y pocas palabras sobre nuestro trabajo futuro.

  • Cómo Triton puede ayudar a analizar binarios ofuscados
    Publicación en : Misc Magazine 82, 2015. [Artículo francés]
    Autores : Jonathan Salwan, Romain Thomas
    Resumen : La ofuscación binaria se utiliza para proteger la propiedad intelectual del software. Existen diferentes tipos de obfucación, pero aproximadamente, transforma una estructura binaria en otra estructura binaria al preservar la misma semántica. El objetivo de la ofuscación es asegurarse de que la información original se "ahogue" en información inútil que dificultará la ingeniería inversa. En este artículo mostraremos cómo podemos analizar un programa de OFR y romper algunas ofuscaciones utilizando el marco Triton.

  • Triton: un marco de ejecución concólica
    Hablar en : SSTIC, Rennes, Francia, 2015. [Documento francés] [Diapositiva en inglés detallada]
    Autores : Jonathan Salwan, Florent Saudel
    Resumen : Esta charla es sobre el lanzamiento de Triton, un marco de ejecución concólica basado en PIN. Proporciona componentes como un motor Taint, un motor de ejecución simbólica dinámica, un motor de instantánea, traducción de la instrucción X64 a SMT2, una interfaz Z3 para resolver restricciones y enlaces de pitón. Según estos componentes, Triton ofrece la posibilidad de crear herramientas para la investigación de vulnerabilidades o asistencia de ingeniería inversa.

  • Análisis de comportamiento dinámico utilizando instrumentación binaria
    Hablar en : St'hack, Burdeos, Francia, 2015. [Diapositiva]
    Autores : Jonathan Salwan
    Resumen : Esta charla puede considerarse como la parte 2 de nuestra charla en SecurityDay. En la parte anterior, hablamos sobre cómo era posible cubrir una función específica en la memoria utilizando el enfoque DSE (ejecución simbólica dinámica). Cubra una función (o sus estados) no significa encontrar todas las vulnerabilidades, cierta vulnerabilidad no bloquea el programa. Es por eso que debemos implementar un análisis específico para encontrar errores específicos. Este análisis se basa en la instrumentación binaria y el análisis de comportamiento de tiempo de ejecución del programa. En esta charla, veremos cómo es posible encontrar estos siguientes tipo de errores: Off-by-uno, desbordamiento de pila / montón, uso gratuito, cadena de formato y {escribir, leer} -what-whwhere.

  • Cubriendo una función utilizando un enfoque dinámico de ejecución simbólica
    Hablar en : Security Day, Lille, Francia, 2015. [Diapositiva]
    Autores : Jonathan Salwan
    Resumen : Esta charla es sobre análisis e instrumentación binaria. Veremos cómo es posible dirigirse a una función específica, instalar la memoria/registros de contexto antes de la función, traducir la instrumentación en una representación intermedia, aplicar un análisis de Taint basado en esta IR, construir/mantener fórmulas para una ejecución simbólica dinámica (DSE), generar un valor concreto para que se repita una ruta específica, restaurar la memoria de contexto/registrar y generar otro valor concreto para pasar otro camino a pasar otro camino de otro camino.

Cita a 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
Información adicional
Aplicaciones relacionadas
Recomendado para ti
Información relacionada Todo