• HOME
  • RESEARCH
  • STUDENTS
  • COURSES
  • HIRING!
  • SEIF: Augmented Symbolic Execution for Information Flow Verification
    K. Ryan, M. Gregoire, C. Sturton.
    Hardware and Architectural Support for Security and Privacy (HASP), 2023.
    Nominated for Best Paper award
    [BibTex]

  • Sylvia: Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs
    K. Ryan, C. Sturton.
    Formal Methods in Computer Aided Design (FMCAD), 2023.
    [GitHub repo] [BibTex]

  • An Intermediate Representation for Hardware Security Verification
    R. Kastner, C. Sturton, C. Deutschbein, A. Meza, K. Ryan, F. Restuccia.
    IEEE VLSI Test Symposium (VTS), 2023.
    [BibTex]

  • Chapter: Information Flow Verification
    C. Sturton, R. Kastner
    Handbook of Computer Architecture,
    Ed. Anupam Chattopadhyay. Springer, June 2022.
    [BibTex]

  • Isadora: Automated Information-Flow Property Generation for Hardware Security Verification
    C. Deutschbein, A. Meza, F. Restuccia, R. Kastner, C. Sturton.
    Journal of Cryptographic Engineering (JCEN), Nov 2022.
    [GitHub repo] [BibTex]

  • Automating Hardware Security Property Generation
    R. Kastner, F. Restuccia, A. Meza, S. Ray, J. Fung, C. Sturton
    Design Automation Conference (DAC), 2022.
    [BibTex]

  • Toward Hardware Security Property Generation at Scale
    C. Deutschbein, A. Meza, F. Restuccia, M. Gregoire, R. Kastner, C. Sturton
    IEEE Security & Privacy Special Issue: Formal Methods at Scale, May/June 2022.
    [BibTex]

  • Isadora: Automated Information Flow Property Generation for Hardware Designs
    C. Deutschbein, A. Meza, F. Restuccia, R. Kastner, C. Sturton
    ACM Workshop on Attacks and Solutions in Hardware Security (ASHES), 2021.
    [GitHub repo] [BibTex]

  • End-to-End Automated Exploit Generation for Processor Security Validation
    R. Zhang, C. Deutschbein, P. Huang, C. Sturton
    IEEE Design & Test Special Issue: Hardware Security Top Picks, 2021.
    Selected as Top Picks in Hardware and Embedded Security, 2021
    [BibTex] [One-minute video] [Decipher article]

  • Evaluating a Specification for its Support of Mode Awareness using Discrete and Continuous Model Checking
    A. Byrnes, C. Sturton
    IEEE International Conference on Intelligent Transportation Systems (ITSC), 2020.
    [BibTex]

  • Evaluating Security Specification Mining for a CISC Architecture
    C. Deutschbein, C. Sturton
    IEEE International Symposium on Hardware Oriented Security and Trust (HOST), 2020.
    [BibTex]

  • Transys: Leveraging Common Security Properties Across Hardware Designs
    R. Zhang, C. Sturton
    IEEE Symposium on Security and Privacy (Oakland), 2020.
    Intel Hardware Security Academic Award, 2nd place ($50,000)
    [BibTex] [One-minute video]

  • FinalFilter: Asserting Security Properties of a Processor at Runtime
    C. Sturton, M. Hicks, S.T. King, J.M. Smith
    IEEE Micro, July/August 2019.
    [BibTex]

  • Mining Security Critical Linear Temporal Logic Specifications for Processors
    C. Deutschbein, C. Sturton
    International Workshop on Microprocessor and SoC Test, Security, and Verification (MTV), 2018.
    [GitHub repo] [BibTeX]

  • End-to-End Automated Exploit Generation for Validating the Security of Processor Designs
    R. Zhang, C. Deutschbein, P. Huang, C. Sturton
    IEEE/ACM International Symposium on Microarchitecture (MICRO), 2018.
    Nominated for Best Paper award
    [Coppelia tool] [Website] [BibTeX]

  • Using a Driver's Eye Data to Predict Accident-Causing Drowsiness Levels
    A. Byrnes, C. Sturton
    IEEE International Conference on Intelligent Transportation Systems (ITSC), 2018.
    [Drowsy Driving Dataset] [BibTex]

  • A Recursive Strategy for Symbolic Execution to Find Exploits in Hardware Designs
    R. Zhang, C. Sturton
    ACM SIGPLAN International Workshop on Formal Methods and Security (FMS), 2018.
    [Website] [BibTex]

  • Identifying Security Critical Properties for the Dynamic Verification of a Processor
    R. Zhang, N. Stanley, C. Griggs, A. Chi, C. Sturton
    ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2017.
    [Website] [Slides] [BibTeX]

  • A System to Verify Network Behavior of Known Cryptographic Clients
    A. Chi, R. A. Cochran, M. Nesfield, C. Sturton, M. K. Reiter
    USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2017.
    [BibTeX]

  • Model Checking to Find Vulnerabilities in an Instruction Set Architecture
    C. Bradfield, C. Sturton
    Short paper, IEEE Symposium on Hardware Oriented Security and Trust (HOST), 2016.
    [BibTeX]

  • Usability of Augmented Reality for Revealing Secret Messages to Users but Not Their Devices
    S.J. Andrabi, M.K. Reiter, C. Sturton.
    Symposium on Usable Privacy and Security (SOUPS), 2015.
    [BibTeX] [Wired article]

  • SPECS: A Lightweight Runtime Mechanism for Protecting Software from Security Critical Processor Bugs
    M. Hicks, C. Sturton, S.T. King, J.M. Smith.
    ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2015.
    [BibTeX]

  • Secure Virtualization with Formal Methods
    C. Sturton
    University of California, Berkeley
    Ph.D. Dissertation, 2013.
    [BibTeX]

  • Symbolic Software Model Validation
    C. Sturton, R. Sinha, T. H.Y. Dang, S. Jain, M. McCoyd, W.-Y. Tan, P. Maniatis, S. A. Seshia, D. Wagner.
    ACM/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE), October 2013.
    [BibTeX]

  • Designing a Voting Machine for Testing and Verification
    C. Sturton
    University of California, Berkeley
    Master's Thesis, 2012.
    [BibTeX]

  • Verification with Small and Short Worlds
    R. Sinha, C. Sturton, P. Maniatis, S. A. Seshia, D. Wagner.
    Formal Methods in Computer-Aided Design (FMCAD), October 2012.
    [Source code] [BibTeX]

  • Automated Analysis of Election Audit Logs
    P. Baxter, A. Edmundson, K. Ortiz, A. M. Quevedo, S. Rodriguez, C. Sturton, D. Wagner.
    USENIX Electronic Voting Technology Workshop/Workshop on Trustworthy Elections (EVT/WOTE), August 2012.
    [AuditBear tool and source code] [BibTeX]

  • Defeating UCI: Building Stealthy and Malicious Hardware
    C. Sturton, M. Hicks, D. Wagner, S. T. King.
    IEEE Symposium on Security and Privacy, May 2011.
    [BibTeX]

  • On Voting Machine Design for Verification and Testability
    C. Sturton, S. Jha, S. A. Seshia, D. Wagner.
    ACM Conference on Computer and Communications Security (CCS), November 2009.
    [BibTeX]

  • Weight, Weight, Don't Tell Me: Using Scales to Select Ballots for Auditing
    C. Sturton, E. Rescorla, D. Wagner.
    USENIX/ACCURATE Electronic Voting Technology Workshop/Workshop on Trustworthy Elections (EVT/WOTE), August 2009.
    [BibTeX]