Computing has advanced to the point where users are often not even aware of the systems they implicitly trust, much less whether those systems deserve that trust. This acceptance puts the onus on suppliers to deal with trust in ways that haven't been expected of them in the past. Designing systems that actually merit trust is critical to living up to user expectations, and continued systems innovation.
In this talk, I'll describe several projects that Galois, a R&D company based in Portland, has done for our clients. I’ll describe our tools for formal verification of imperative code, and how we have applied them to successfully verify a high-performance implementation of a digital signature implementation based on elliptic curves. I'll also describe recent work on virtualization in mobile phones, higher assurance UAV control software, and recent applications of computing on encrypted data.
These projects have divergent goals and technology approaches, but each is related to trusted systems. I hope to provide a grounded picture of the role of trust in systems, and foster discussion about how different lines of research connect to overarching goals of building trusted and trustworthy systems.