Software today comes with few, if any, security guarantees. Traditionally, software vendors become aware of vulnerabilities after an attack occurs and then issue a patch that fixes that particular attack. CyLab researchers are looking to change all of that by employing mathematical techniques, commonly referred to as formal methods, to mathematically prove that a system is secure and protected against cyberattacks.
Formal methods @ CyLab
Fourteen years later, Pasareanu’s automated software-testing work awarded for retrospective impact
Fourteen years ago, CyLab associate research professor Corina Pasareanu and two of her colleagues published a paper outlining three automated techniques for checking software for bugs and vulnerabilities. This team received the 2018 Retrospective Impact Award from the International Symposium on Software Testing and Analysis (ISSTA).
Bryan Parno shares Distinguished Paper Award win with demonstration of verifiable security
Chances are, you’re reading this article on a web browser that uses HTTPS, the protocol over which data is sent between a web browser and the website users are connected to. In fact, nearly half of all web traffic passes through HTTPS. Despite the “S” for security in “HTTPS,” this protocol is far from perfectly secure.
Helping users manage online data
The data you give to Facebook or Fitbit might be less secure than you think, but CyLab's Lujo Bauer, Associate Professor of Electrical and Computer Engineering and in the Institute for Software Research, wants to give you more control over your information by mathematically proving privacy systems work.
Turning mathematics into software
What keeps self-driving cars from rear-ending other cars on the road? Math. In our latest video, CyLab's Franz Franchetti, Associate Professor of the Department of Electrical and Computer Engineering, discusses turning mathematics into software in order to prevent autonomous cars from causing accidents on the road.