Paper Info
Title
Digital system robustness via design constraints: The lesson of formal methods
Abstract
Current programming languages and programming models make it easy to create software and hardware systems that fulfill an intended function but also leave such systems open to unintended function and vulnerabilities. Software engineering and code hygiene may make systems incrementally safer, but do not produce the wholesale change necessary for secure systems from the outset. Yet there exists an approach with impressive results: We cite recent examples showing that formal methods, coupled with formally informed digital design, have produced objectively more robust code even beyond the properties directly proven. Though discovery of zero-day vulnerabilities is almost always a surprise and powerful tools like semantic fuzzers can cover a larger search space of vulnerabilities than a developer can conceive of, formal models seem to produce robustness of a higher qualitative order than traditionally developed digital systems. Because the claim is necessarily a qualitative one, we illustrate similar results with an idealized programming language in the form of Boolean networks where we have control of parameters related to stability and adaptability. We argue that verifiability with formal methods is an instance of broader design constraints that promote robustness. We draw analogies to real-world programming models and languages that can be mathematically reasoned about in contrast to ones that are essentially undecidable.
Year
DOI
Venue
2015
10.1109/SYSCON.2015.7116737
SysCon
Keywords
Field
DocType
digital design,complex systems,formal methods,programming models,robustness,security,computer languages,adaptability,computational modeling,formal verification,boolean functions,programming,stability,programming languages,hardware,software engineering,high level languages
Second-generation programming language,Programming language,Programming paradigm,Software engineering,Computer science,Design by contract,Inductive programming,Formal methods,Programming language theory,Computer programming,Software development
Conference
ISSN
Citations 
PageRank 
1944-7620
0
0.34
References 
Authors
17
3
Name
Order
Citations
PageRank
Jackson Mayo1437.97
Robert C. Armstrong210021.51
Geoffrey C. Hulette363.88