A formal methods safe harbor

We discuss a problem: Internet of Things devices running software are vulnerable to accidents and exploitation, a technology solution: preventing exploitable bugs by developing machine-checked proofs of software correctness and security, and a policy lever to incentivize adoption of this solution: a safe harbor from FTC unfairness prosecution for manufacturers that use formal methods to guarantee safer, more secure devices. To motivate the potential of formal methods, we present a technical contribution: a formally verified connected lightbulb switch, proven immune to certain types of software exploits. We discuss a framework, the Common Weakness Enumeration, that the FTC and manufacturers could use as a shared language to explain what classes of software vulnerability a manufacturer will defend against. We outline the authority of the FTC in regards to poor data security practices as unfair practices and how our safe harbor would both provide immunity to participants and be updated over time to continue to incentivize ever stronger software protections.

Name thesis:degree_name

Master

Department dc:contributor.department

Massachusetts Institute of Technology. Institute for Data, Systems, and Society

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2019

Author dc:creator

• Wood, Clark,S. M.Massachusetts Institute of Technology.

Advisor dc:contributor.advisor

• Daniel Weitzner and Adam Chlipala.

• Institute for Data, Systems, and Society.
• Technology and Policy Program.

Statement dc:rights

• MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

https://hdl.handle.net/1721.1/122219

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/122219