Minimal Specifications for Detecting Security Vulnerabilities
Computers are nearly ubiquitous in modern society with uses from maintaining friendships and monitoring homes to managing money and coordinating health care. As the roles of a computer continue to expand, so to does the threat posed by cyberattacks. An important challenge for today’s software engineers is to build secure software and help neutralize these threats. Formal methods have long been suggested as an excellent way to build secure software but have not been widely adopted for this purpose. The ``conventional wisdom'' has suggested several reasons for this slow adoption, including a steep learning curve, difficulty in augmenting existing systems, and lack of tools with security-specific abstractions. Our hypothesis, however, is that applying a small and easy to learn subset of the techniques available today could significantly decrease software vulnerabilities and reduce the risk of cyberattacks. In this paper, we discuss the motivation for our hypothesis and discuss our ongoing experiment to test it.
Mon 5 NovDisplayed time zone: Guadalajara, Mexico City, Monterrey change
15:30 - 17:00
|SPARK by Example: an introduction to formal verification through the standard C++ library|
|Soundness of a Dataflow Analysis for Memory Monitoring|
|Minimal Specifications for Detecting Security Vulnerabilities|
|6:30PM HILT Banquet at Legal Seafoods, Park Plaza, preceded by SIGAda EC meeting from 5:15 to 6:15PM|