Write a Blog >>

It is well understood that many cyber-physical systems incorporate software that is getting increasingly complex, hard to manage, and therefore often quite fragile. We will present our recent work on addressing this challenge using formal methods based tools and techniques for creation of software for cyber-physical systems that provide strong assurances that the resulting software would be secure, safe, and reliable.

These include - the use of a formally verified operating system; - the use of a toolchain where proofs of controller safety properties in a theorem prover for hybrid systems are used for synthesis of high assurance high performance control code implementations; - leveraging general-purpose formal tools to create automated synthesizers for high assurance message handling code that comes with proofs of correctness (which imply absence of misbehaviors due to e.g. malformed messages); and - tools for producing high assurance and medium assurance glue code that links different modules in a secure safe and resilient manner.

This talk will primarily present a tool user perspective – outlining how we applied these tools and describing both successes and challenges of this effort.

Thu 22 Jun

dsw-2017-papers
10:30 - 12:10: DSW 2017 - Academic crypto projects; industry perspective on formal-methods integration at Vertex WS216
Chair(s): Zhong ShaoYale University
dsw-2017-papers10:30 - 11:00
Talk
Adam ChlipalaMassachusetts Institute of Technology, USA
dsw-2017-papers11:00 - 11:30
Talk
Lennart BeringerPrinceton University
dsw-2017-papers11:30 - 12:10
Talk
Aleksey NoginHRL Laboratories, LLC