| Conference: | Verification Futures 2018 (click here to see full programme) |
| Speaker: | Roderick Chapman, Independent Consultant Software Engineer, Protean Code Limited |
| Presentation Title: | Development and Formal Verification of Secure Updates for Embedded Systems |
| Abstract: | Your smartphone (and some brands of car) appear to be able to update their operating system and applications securely, remotely and wirelessly. Can the same capability be brought to deeply embedded, critical systems? The benefits are numerous, most notably bringing the potential to upgrade the capability of systems ‘in the field’ without need for a physical recall to the factory or a maintenance facility.
This talk will outline the technologies behind the scenes of such a ‘code signing’ infrastructure, including the cryptographic primitives and protocols needed to assure the confidentiality, integrity and authentication of such updates. An implementation sets some serious challenges, including the need to run on small ‘bare metal’ target machines, atomicity of the update process, and the need to meet the highest cryptographic and technical standards. We will also consider the formal verification of the software, including flow analysis, theorem proving, and worst-case analysis for memory usage.
|
| Speaker Bio: | Roderick Chapman is an independent consultant software engineer. He specialises in the development of safety and security-critical systems, from requirements engineering, through architectural design and implementation, to verification, audit and assessment. Following graduation from the University of York, Rod joined Praxis (now Altran UK), and contributed to many of the company’s keynote projects, rising to the role of principal engineer for software process and design. He also led the programming language and verification research group at Praxis, leading the technical development, training, sales and marketing of the SPARK product line. Rod is a regular speaker at international conferences, and is widely recognized as a leading authority on high-integrity software development, programming language design, and software verification tools. In 2006, he was invited to become a Fellow of the British Computer Society. In 2011, Rod was the joint recipient of the inaugural Microsoft Research Verified Software Milestone Award for his contribution to the Tokeneer project. In February 2015, Rod was appointed Honorary Visiting Professor in the Department of Computer Science at the University of York |
