Nestan Tsiskaridze, University of California, Santa Barbara
The modern world critically depends on the security and safety of software. We seek to ensure customer confidence and protect privacy, intellectual property, and national security. As threats to software security have become more sophisticated, so too have the techniques developed to ensure security.
This talk focuses on novel opportunities to automate bug detection and security exploit generation provided by advances in symbolic execution and automated constraint solving. It discusses how symbolic execution can benefit from novel techniques in Satisfiability Modulo Theories (SMT), a subfield of automated theorem proving that in the past 10 years has revolutionized the discipline. The talk presents a recent highly successful application of SMT solvers in support of the security analysis of Web applications and how these new capabilities open opportunities for automating such analysis beyond the Web.
This is a joint work with Clark Barrett (NYU/Stanford University), Morgan Deters (NYU), Tianyi Liang (The University of Iowa), Andrew Reynolds (The University of Iowa/EPFL), and Cesare Tinelli (The University of Iowa).
Nestan is a Postdoctoral Researcher at the Department of Computer Science at the University of California, Santa Barbara. Her research interests include Automated Reasoning, Satisfiability Modulo Theories, Formal Verification, and Security. Her current work focuses on developing symbolic analysis techniques and tools for automatic identification of vulnerabilities in Java bytecode. Previously she worked on developing techniques to aid checking of software security properties, automating solving of string constraints; and on automated reverse engineering of integrated circuits for security analysis.
She was a Postdoctoral Researcher and a Visiting Assistant Professor at the University of Iowa and a Postdoctoral Researcher at Princeton University.
She received a PhD in Computer Science from the University of Manchester, United Kingdom. Her dissertation presented a novel approach for Linear Programing—the Conflict Resolution method.
Enigma is a registered trademark of the USENIX Association.