This talk will go over our approach to the development and verification of post-quantum cryptographic code at AWS. It will cover our approach to assembly-language verification, and how we are verifying C code within AWS LibCrypto. Proof also enables “fearless optimization” of crypto code, where proofs of correctness and/or equivalence preserve functional behaviour while allowing and inspiring non-trivial performance improvements. We’ll go on to talk about how AI agents are transforming our productivity and developer engagement without compromising our stratospheric quality bar. Our approach combines automated reasoning guardrails that constrain AI behaviour to known-good outcomes with aggressive use of agents to find proofs and optimizations of our most critical code.
Dr. Rod Chapman is a senior principal applied scientist within the Cryptography group of Amazon Web Services. He specializes in the design, development and verification of cryptographic software, and has particular experience with programming language design and automated reasoning technologies. He also coaches development teams and leadership in high-assurance software development disciplines, technologies, and processes. He is a Fellow of the IET and an honorary visiting professor at the University of York.
Reality Check: Independent Evaluation of Modern Grey-Box Fuzzing Techniques Pavel Frolikov
2
Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation Priscilla Kyei Danso, Mohammad Saqib Hasan, Niranjan Balasubramanian, and Omar Chowdhury
3
CFIghter: Automated Control-Flow Integrity Enablement and Evaluation for Legacy C/C++ Systems Sabine Houy, Bruno Kreyssig, and Alexandre Bartel
4
SoK: A Modularized Framework for Symbolic Execution and Application for Usable Tool Design James Mattei, Andrew Lin, Jasper Geer, Jie Hu, Moritz Schloegel, Tiffany Bao, and Daniel Votipka
Dr. Rod Chapman, Senior Principal Applied Scientist, Amazon Web Services
2
Dr. Roland Yap Hock Chuan, Associate Professor, Computer Science, School of Computing, National University of Singapore
3
Dr. Amin Milani Fard, Associate Professor, Computer Science, College of Engineering & Computing Sciences, New York Institute of Technology – Vancouver Campus
4
Dr. Venkat Sai Suman Lamba Karanam, Assistant Professor, Computer Science, College of Arts and Sciences, Bowling Green State University
5
Marcelo Garcia, Cyber Security Policy and Strategy Specialist, Brazil Federal Fluminense University
Origin Story: A Comprehensive Lifecycle Analysis of Same-Origin Policy Bugs Jakub Szymsza, Gertjan Franken, Vik Vanderlinden, Tom Van Goethem, Mathy Vanhoef, and Lieven Desmet
2
ASN1spect: Uncovering ASN.1 Compiler-Generated Vulnerabilities in Critical Infrastructure Seaver Thorn, Nathaniel Bennett, Kevin Butler, Patrick Traynor, and William Enck
3
On the Variability of Source Code in Maven Package Rebuilds Jens Dietrich and Behnaz Hassanshahi
4
RepliGuard: Policy-Driven Replica Management Framework for Protecting against Acoustic Attacks Jennifer Sheldon, Yungwoo Ko, Sri Hrushikesh Varma Bhupathiraju, Sara Osmanovic, Weidong Zhu, Md Jahidul Islam, and Sara Rampazzi
5
At the Precipice of Integrity Protection using Pointer Authentication Viorel Preoteasa, Carlos Chinea Pérez, Hans Liljestrand, and Jan-Erik Ekberg
6
Cloud Safety: A Hardware Perspective Raghudeep Kannavara, Matthew Dickinson, and Monty Wiseman
Mon 6 Jul
Displayed time zone: Eastern Time (US & Canada)change
The gap between our capabilities to build software and to understand what we’ve built, reason about it, and anticipate its emergent behaviors, is tremendous. The joint “Closing the Software Understanding Gap” memorandum by US Government agencies recognized addressing this gap as a national priority. I will argue that the keys to bridging this gap lie in rethinking ostensibly mere-engineering tasks as truly first-class computer science challenges; changing the formats in which code and data are delivered based on this new understanding; and applying strong predictive theories of software’s emergent behaviors (typically witnessed via ‘hacking’ or exploitation) to all stages of software construction, delivery, and operation.
Dr. Sergey L. Bratus is the Dartmouth College Distinguished Professor in Cyber Security, Technology, and Society and an Associate Professor of Computer Science. In 2018–2024 he served as a Program Manager at DARPA’s Information Innovation Office (I2O), where he created multiple fundamental research programs in cybersecurity, resilience, and sustainment of critical software.
OpenClaw RedTeam Recon: A Local OSS-LLM-Powered Autonomous Reconnaissance Agent Marcelo Garcia and Robson de Oliveira Albuquerque
2
SafeAIMerge: A Tool for Integrating DAST and LLM-Generated Security Feedback into GitHub Actions Workflows Arpit Thool, Justin Smith, and Chris Brown
3
A CNN-LSTM Security Model for SCADA Network Olga Dye and Brian Dye
4
SoK: A Comprehensive Analysis of the Current Status of Neural Tangent Generalization Attacks with Research Directions Thushari Hapuarachchi and Kaiqi Xiong
SGX-MB: A Secure Framework for Middleboxes Leveraging Intel SGX Mahmoud Hofny, Lianying Zhao, and Amr Youssef
2
A Technology-Readiness Evaluation of Private Set Intersection Wout Ceulemans, Pieter Philippaerts, Dimitri Van Landuyt, and Wouter Joosen
3
Augment Mutual TLS Authentication with HW Rooted Identity: Simplified Device Lifecycle and Interoperability Dhananjay Phadke and Xiling Sun
4
Adversarially Mixed Secret Key Generation for Side-Channel Defense for the Cloud Venkat Sai Suman Lamba Karanam, Zahmeeth Sayed Sakkaff, and Pasindu Balasooriya