Formalizing attacks and extracting application models for security model checkers

(CSE Colloquium Lecture Series)

Marius Minea
Marius Minea

Marius Minea
Current Affiliation: Politehnica University of Timisoara, Romania
Friday, March 2, 2018, 11:00am
Room 1242, CSE Building

Formalizing attacks and extracting application models for security model checkers

Abstract: While model checkers have a long use in verifying security protocols for properties like confidentiality, integrity, or authentication, checking other interesting properties is often done with special analyses and not automated. I will discuss how to model denial of service and guessing attacks by augmenting the capabilities of the classical Dolev-Yao attacker with specialized deduction rules. This allows automated detection of these attacks by off-the-shelf model checkers. Second, I will present how to extract formal models from web applications using JavaServer Pages, with a tool that includes support for SQL queries and user-specified abstractions. This provides an automated verification pipeline from application code to security model checkers, capable of detecting, e.g., session management flaws. I will also briefly discuss ongoing work, including differential testing and dynamic taint analysis for error localization.

Bio: Marius Minea is an associate professor at the Politehnica University of Timisoara, Romania. He received his PhD from Carnegie Mellon with a thesis on model checking for timed systems, advised by Ed Clarke and was then a postdoctoral researcher at the University of California, Berkeley. His research interests are at the intersection of software analysis, testing and security, where he has led several research projects. He is teaching courses on verification and security, enjoys using live coding in programming classes and has designed a discrete structures course that uses functional programming.