Presented at
DEF CON 30 (2022),
Aug. 14, 2022, 11 a.m.
(45 minutes).
For decades, software vulnerabilities have remained an unsolvable security problem regardless of years of investment in various mitigations, hardening and fuzzing strategies. In the last years there have been moves to formal methods as a path toward better security. Verification and formal methods can produce rigorous arguments about the absence of the entire classes of security bugs, and are a powerful tool to build highly secure software.
AdaCore/SPARK is a formally defined programming language intended for the development of high integrity software used in systems where predictable and highly reliable operation is crucial. The formal, unambiguous, definition of SPARK allows a variety of static analysis techniques to be applied, including information flow analysis, proof of absence of run-time exceptions, proof of termination, proof of functional correctness, and proof of safety and security properties.
In this talk we will dive-into AdaCore/SPARK, cover the blind spots and limitations, and show real-world vulnerabilities which we met during my work and which are still possible in the formally proven software. We will also show an exploit targeting one of the previously described vulnerabilities.
Presenters:
-
Alex Tereshkin
- Principal System Software Engineer (Offensive Security)
Alex Tereshkin is an experienced reverse engineer and an expert in UEFI security, Windows kernel and hardware virtualization, specializing in rootkit technologies and kernel exploitation. He has been involved in the BIOS and SMM security research since 2008. He is currently working as a Principal Offensive Security Researcher at NVIDIA. He has done significant work in the field of virtualization-based malware and Windows kernel security. He is a co-author of a few courses taught at major security conferences and a co-author of the first UEFI BIOS and Intel ME exploits.
-
Adam Zabrocki / pi3
- Principal System Software Engineer (Offensive Security) at NVIDIA
as Adam 'pi3' Zabrocki
Adam Zabrocki 'pi3' is a computer security researcher, pentester and bughunter, currently working as a Principal Offensive Security Researcher at NVIDIA. He is a creator and developer of Linux Kernel Runtime Guard (LKRG) - his moonlight project defended by Openwall. Among others, he used to work in Microsoft, European Organization for Nuclear Research (CERN), HISPASEC Sistemas (known from the virustotal.com project), Wroclaw Center for Networking and Supercomputing, Cigital. The main area of his research is low-level security (CPU arch, uCode, FW, hypervisor, kernel, OS).
As a hobby, he was a developer in The ERESI Reverse Engineering Software Interface project, a bughunter (discovered vulnerabilities in Hyper-V, KVM, RISC-V ISA, Intel's Reference Code, Intel/NVIDIA vGPU, Linux kernel, FreeBSD, OpenSSH, gcc SSP/ProPolice, Apache, Adobe Acrobat Reader, Xpdf, Torque GRID server, and more) and studied exploitation and mitigation techniques, publishing results of his research in Phrack Magazine.
Adam is driving Pointer Masking extension for RISC-V, he is a co-author of a subchapter to Windows Internals and was The Pwnie Awards 2021 nominee for most under-hyped research. He was a speaker at well-known security conferences including Blackhat, DEF CON, Security BSides, Open Source Tech conf and more.
Links:
Similar Presentations: