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.

Journal Articles:

# Title (click for html version) Formats Published In Date Comments
1 InterAspect: Aspect-Oriented Instrumentation with GCC PDF BibTeX Internation Journal on Formal Methods in System Design Sep 2012  
2 Software Monitoring with Controllable Overhead PS PDF BibTeX International Journal on Software Tools for Technology Transfer (STTT) Dec 2010  

Conference and Workshop Papers:
# Title (click for html version) Formats Published In Date Comments
1 Redflag: A framework for analysis of kernel-level concurrency PS PDF BibTeX 11th International Conference on Algorithms and Architectures for Parallel Processing (ICA3PP'11) Oct 2011  
2 Runtime verification with state estimation PS PDF BibTeX 2nd International Conference on Runtime Verification (RV 2011) Sep 2011 Won Best Paper Award
3 Aspect-Oriented Instrumentation with GCC PS PDF BibTeX 1st International Conference on Runtime Verification (RV 2010) Nov 2010 Released as open source.
4 The Visual Development of GCC Plug-ins PS PDF BibTeX Proceedings of the 2009 GCC Developers' Summit Jun 2009  
5 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  
6 Extending GCC with Modular GIMPLE Optimizations PS PDF BibTeX Proceedings of the 2007 GCC Developers' Summit Jul 2007  
7 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  
8 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  
9 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  
10 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 Runtime Verification of Kernel-Level Concurrency Using Compiler-Based Instrumentation PS PDF BibTeX Stony Brook U. CS TechReport FSL-12-05 Dec 2012 Ph.D. Dissertation
2 Stopping Data Races Using Redflag PS PDF BibTeX Stony Brook U. CS TechReport FSL-10-02 May 2010 M.S. Thesis
3 Flexible Debugging with Controllable Overhead PS PDF BibTeX Stony Brook U. CS TechReport FSL-09-01 Aug 2009 Ph.D. Thesis
4 The Visual Development of GCC Plug-ins with GDE, PS PDF BibTeX Stony Brook U. CS TechReport FSL-09-04 Apr 2009 M.S. Thesis
5 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)

Past Students:

# Name (click for home page) Program Period Current Location
1 Sean Callanan PhD Sep 2003 - Aug 2009 System Software Engineer, Pixel Hardware Group, Google (Mountain View, CA)
2 Justin Seyster PhD Jan 2006 - Dec 2012 Software Engineer, Query Team at MongoDB (New York, NY)
3 Daniel J. Dean MS Sep 2007 - Jun 2009 Research Staff Member, IBM Watson Health Cloud (Yorktown Heights, NY)
4 Abhinav Duggal MS Sep 2008 - May 2010 Senior Software Engineer, Filesystems Group EMC/DataDomain (Bangalore, India)
5 Mandar S Joshi MS Sep 2011 - Dec 2012 Member of Technical Staff, Granite Group at Riverbed (Sunnyvale, CA)
6 Atul Karmarkar MS Jan 2012 - Dec 2012 Sr. Software Engineer, Core File Systems Group, EMC Data Domain (Santa Clara, CA).
7 Samriti Katoch MS Sep 2010 - Dec 2011 System Software Engineer, Platform Engineering Group at Akamai (Cambridge, MA)
8 Nishant Nagalia MS Sep 2002 - May 2004 Software Engineer, Ashley Laurent (Austin, TX)
9 Amit Purohit MS Sep 2001 - May 2003 Ananda Center in India (India)
10 Prabakar Radhakrishnan MS Jan 2010 - Dec 2010 Software Engineer, Search Quality group Google (Mountain View, CA)
11 Siddhi Tadpatrikar MS Jan 2011 - Dec 2011 Senior Staff Software Engineer (Senior Engineering Manager), Google Inc. (Mountain View, CA)
12 Daniel J. Dean BS May 2006 - Aug 2007 Research Staff Member, IBM Watson Health Cloud (Yorktown Heights, NY)
13 Scott Harvey BS Aug 2014 - Dec 2014  
14 Dung Phan temp-PhD Mar 2014 - May 2015  
15 Abhishek Rai temp-PhD Sep 2003 - Aug 2005 Principal Engineer, ThoughtSpot Inc. (Palo Alto, CA)
16 Junxing "Jesse" Yang temp-PhD Apr 2015 - May 2015  

Sponsors:

# Sponsor Amount Period Type Title (click for award abstract)
1 U.S. Air Force Office of Scientific Research $620,861 2014-2016 Co-PI Adaptive Runtime Verification and Recovery for Mission-Critical Software
2 U.S. Air Force Office of Scientific Research $881,691 2009-2012 Co-PI Survivable Software
3 NSF CSR--AES $830,000 2005-2009 Lead-PI CSR--AES: Runtime Monitoring and Model Checking for High-Confidence System Software