High Confidence Operating Systems

Operating System development is difficult; debugging OSs is a daunting challenge, especially considering the hostile kernel environment and the amount of concurrency that takes place. A stable OS is crucial, especially in light of today's attackers who are looking for any way to exploit bugs to gain unauthorized access. In this project we apply formal verification techniques, using Concurrent Class Machines (CCMs) to verify that kernel code confirms to system call specifications. We verify that no sequence of system calls, with any input, could potentially leave the OS in an inconsistent state or crash the OS. We explore static techniques at compile time, dynamic techniques at run time, slicing as a way to focus on specific aspects of the kernel code (e.g., locking semantics, reference counting consistency, etc.).

See also the overall HCOS project Web page.

Conference and Workshop Papers:

# Title (click for html version) Formats Published In Date Comments
1 Software Monitoring with Bounded Overhead BibTeX NSF Next Generation Software Workshop (NSF NGS 2008) held in conjunction with the 22st IEEE International Parallel and Distributed Processing Symposium (IPDPS 2008) Apr 2008  
2 Extending GCC with Modular GIMPLE Optimizations PS PDF BibTeX Proceedings of the 2007 GCC Developers' Summit Jul 2007  
3 Model Predictive Control for Memory Profiling PS PDF BibTeX NSF Next Generation Software Workshop (NSF NGS 2007) held in conjunction with the 21st IEEE International Parallel and Distributed Processing Symposium (IPDPS 2007) Mar 2007  
4 Compiler-Assisted Software Verification Using Plug-Ins PS PDF BibTeX NSF Next Generation Software Workshop (NSF NGS 2006) held in conjunction with the 20th IEEE International Parallel and Distributed Processing Symposium (IPDPS 2006) Apr 2006  
5 Efficient and Safe Execution of User-Level Code in the Kernel PS PDF BibTeX NSF Next Generation Software Workshop, in conjunction with IPDPS 2005 Apr 2005  
6 High-Confidence Operating Systems PS PDF BibTeX Tenth ACM SIGOPS European Workshop Sep 2002  

Technical Reports:

# Title (click for html version) Formats Published In Date Comments
1 On the Role of Static Analysis in Operating System Checking and Runtime Verification PS PDF BibTeX Stony Brook U. CS TechReport FSL-05-01 May 2005 Ph.D. Research Proficiency Exam (RPE)

Current Students:

# Name (click for home page) Program Member Since
1 Sean Callanan PhD Sep 2003
2 Justin Seyster PhD Jan 2006
3 Daniel J. Dean MS Sep 2007
4 Abhinav Duggal MS Sep 2008

Past Students:

# Name (click for home page) Program Period Current Location
1 Abhishek Rai PhD Sep 2003 - Aug 2005 Member of the Technical Staff, Structured Data Access group, VMware, Inc. (Palo Alto, CA)
2 Nishant Nagalia MS Sep 2002 - May 2004 Software Engineer, Ashley Laurent (Austin, TX)
3 Amit Purohit MS Sep 2001 - May 2003 Technical Staff Member, IBM India Research Lab (New Delhi, India)
4 Daniel J. Dean BS May 2006 - Aug 2007 Stony Brook U. CS M.S. program (Stony Brook, NY)

Sponsors:

# Sponsor Amount Period Type Title (click for award abstract)
1 NSF CSR--AES $830,000 2005-2009 PI CSR--AES: Runtime Monitoring and Model Checking for High-Confidence System Software

(Last updated: Tue Dec 9 20:15:20 EST 2008)