How to Lift and Verify Differential Equations from Machine Code of Cyber-Physical Systems

Abstract

En este proyecto de Fin de Grado, se ha desarrollado una herramienta, denominada “InteGreat”, que obtiene las ecuaciones de control de dispositivos embebidos y las representa en un lenguaje de alto nivel como Python. Mediante técnicas de ingeniería inversa y ejecución simbólica, partiendo del código binario del dispositivo, se analiza dicha memoria, y se ejecuta una inferencia de las ecuaciones de control hasta un lenguaje de programación de alto nivel o de dominio específico. De esta manera, se representan de manera simple y en formato ejecutable los cálculos y ecuaciones que gobiernan los bucles de control del dispositivo ciber-físico en cuestión, por lo que se podrán identificar vulnerabilidades y errores de programación con el objetivo de mejorar la ciberseguridad y calidad funcional del mismo. Esta metodología se ha aplicado a dos sistemas embebidos para demostrar su utilidad. El primero de ellos, es un quadricóptero, del que se obtuvieron las ecuaciones de filtrado de los sensores. Una vez obtenidas, se realizo el análisis de accesibilidad de estados, verificando el comportamiento idéntico del filtro tanto en la simulación como en el propio dispositivo. En segundo lugar, se realizó con éxito el análisis de un PLC, obteniendo a su vez las ecuaciones que controlan su salida y entrada. Con ello, se realizó una simulación de un ciber-ataque conocido contra una planta química obteniendo un resultado esperado y pudiendo completar dicho ciber-ataque.

In this project, “InteGreat” was developed to obtain the control equations of embedded systems and represent them in a high-level programming language like Python. Through the use of reverse engineering and symbolic execution, using the device’s binary code, the memory is analyzed and the control equations are inferred up to a high-level or domain-specific programming language. By means of this tool which is built with state-of-the-art libraries, the equations and calculations that govern the control loops of the cyber-physical devices are presented in an easy executable way. With this project it will be easy to identify vulnerabilities and programming errors with the objective of improving device cybersecurity and functional quality. This methodology was applied to two embedded systems to demonstrate the tool’s capabilities. The first one is a drone, whose sensor filtering equations were obtained. Once lifted, a reachability analysis was performed, verifying the correct behavior of both, the simulation and the physical device. Secondly, the analysis of a PLC was performed, lifting the equations that govern its inputs and outputs. With those, a known cyber-attack simulation was performed against a chemical process, obtaining an expected result, and completing successfully that cyber-attack.