Steve's research focuses on the problem of building software that is reliable, robust, and secure by construction. He draws on techniques from type theory, logic, and formal methods to develop programming languages that enforce strong information-flow and authorization policies in dynamic, distributed environments. His recent projects have developed techniques for incorporating robust declassification, dynamic principals, and cryptographic enforcement of authorization policies into a security-oriented language called AURA. Steve is also interested in machine-checked theorem proving, concurrent programming, and functional languages.