BEGIN:VCALENDAR
VERSION:2.0
PRODID:Data::ICal 0.24
BEGIN:VEVENT
DESCRIPTION:   'Title: Exploitation in the era of formal verification: a pe
 ek at a\n   new frontier with AdaCore/SPARK\n   When: Sunday\, Aug 14\, 11
 :00 - 11:45 PDT\n   Where: Caesars Forum - Forum 104-105\, 135-136 (Track 
 1) - [1]Map\n   Speakers:Adam 'pi3' Zabrocki\,Alex Tereshkin\n\n   Speaker
 Bio:Adam 'pi3' Zabrocki \, Principal System Software Engineer\n   (Offensi
 ve Security)\n   Adam Zabrocki 'pi3' is a computer security researcher\, p
 entester and\n   bughunter\, currently working as a Principal Offensive Se
 curity\n   Researcher at NVIDIA. He is a creator and developer of Linux Ke
 rnel\n   Runtime Guard (LKRG) - his moonlight project defended by Openwall
 .\n   Among others\, he used to work in Microsoft\, European Organization 
 for\n   Nuclear Research (CERN)\, HISPASEC Sistemas (known from the\n   vi
 rustotal.com project)\, Wroclaw Center for Networking and\n   Supercomputi
 ng\, Cigital. The main area of his research is low-level\n   security (CPU
  arch\, uCode\, FW\, hypervisor\, kernel\, OS).\n\n   As a hobby\, he was 
 a developer in The ERESI Reverse Engineering\n   Software Interface projec
 t\, a bughunter (discovered vulnerabilities in\n   Hyper-V\, KVM\, RISC-V 
 ISA\, Intel's Reference Code\, Intel/NVIDIA vGPU\,\n   Linux kernel\, Free
 BSD\, OpenSSH\, gcc SSP/ProPolice\, Apache\, Adobe\n   Acrobat Reader\, Xp
 df\, Torque GRID server\, and more) and studied\n   exploitation and mitig
 ation techniques\, publishing results of his\n   research in Phrack Magazi
 ne.\n\n   Adam is driving Pointer Masking extension for RISC-V\, he is a\n
    co-author of a subchapter to Windows Internals and was The Pwnie\n   Aw
 ards 2021 nominee for most under-hyped research. He was a speaker at\n   w
 ell-known security conferences including Blackhat\, DEF CON\, Security\n  
  BSides\, Open Source Tech conf and more.\n\n   Twitter: [2]@Adam_pi3\n\n 
   SpeakerBio:Alex Tereshkin \, Principal System Software Engineer\n   (Off
 ensive Security)\n   Alex Tereshkin is an experienced reverse engineer and
  an expert in\n   UEFI security\, Windows kernel and hardware virtualizati
 on\,\n   specializing in rootkit technologies and kernel exploitation. He 
 has\n   been involved in the BIOS and SMM security research since 2008. He
  is\n   currently working as a Principal Offensive Security Researcher at\
 n   NVIDIA. He has done significant work in the field of\n   virtualizatio
 n-based malware and Windows kernel security. He is a\n   co-author of a fe
 w courses taught at major security conferences and a\n   co-author of the 
 first UEFI BIOS and Intel ME exploits.\n   Twitter: [3]@AlexTereshkin\n\n 
   Description:\n   For decades\, software vulnerabilities have remained an
  unsolvable\n   security problem regardless of years of investment in vari
 ous\n   mitigations\, hardening and fuzzing strategies. In the last years 
 there\n   have been moves to formal methods as a path toward better securi
 ty.\n   Verification and formal methods can produce rigorous arguments abo
 ut\n   the absence of the entire classes of security bugs\, and are a powe
 rful\n   tool to build highly secure software.\n\n   AdaCore/SPARK is a fo
 rmally defined programming language intended for\n   the development of hi
 gh integrity software used in systems where\n   predictable and highly rel
 iable operation is crucial. The formal\,\n   unambiguous\, definition of S
 PARK allows a variety of static analysis\n   techniques to be applied\, in
 cluding information flow analysis\, proof\n   of absence of run-time excep
 tions\, proof of termination\, proof of\n   functional correctness\, and p
 roof of safety and security properties.\n\n   In this talk we will dive-in
 to AdaCore/SPARK\, cover the blind spots\n   and limitations\, and show re
 al-world vulnerabilities which we met\n   during my work and which are sti
 ll possible in the formally proven\n   software. We will also show an expl
 oit targeting one of the previously\n   described vulnerabilities.\n\n   '
 \n\n   1. https://defcon.outel.org/consolidated_page.html#CaesarsForumBR\n
    2. https://twitter.com/Adam_pi3\n   3. https://twitter.com/AlexTereshki
 n\n\n\n
DTEND:20220814T184500Z
DTSTART:20220814T180000Z
LOCATION:DC - Caesars Forum - Forum 104-105\, 135-136 (Track 1)
SUMMARY:Exploitation in the era of formal verification: a peek at a new fro
 ntier with AdaCore/SPARK
END:VEVENT
END:VCALENDAR