Pic_ChapinAbstract: Assuring System Components Using Formal Methods 

Recent advances in the application of automated theorem provers to the development of systems software have allowed us to develop the Syracuse Assured Boot Loader Executive (SABLE).  We are developing proofs that SABLE performs correctly, i.e., that it will only boot code that is verified correct by an authorized user during configuration.  In this talk, I will describe the development environment and  methodology we are using, and outline our strategy for proving SABLE’s correctness.


Steve Chapin is an Associate Professor in the Department of Electrical Engineering and Computer Science at Syracuse University.  His research interests include multiple aspects of computer security, including systems assurance grounded on formal methods and security in the Internet of Things (especially devices for the Smart Grid and charging and discharging of electric vehicles).  He received his PhD in Computer Sciences from Purdue University, and a dual B.S. in Computer Science and Mathematics from Heidelberg College.