High-confidence operating systems
Authors: 
Radu Grosu, 
Erez Zadok, Scott A. Smolka, Rance Cleaveland, Yanhong A. LiuAuthors Info & Claims
Pages 205 - 208
Abstract
Operating systems (OSs) are among the most sophisticated software systems in widespread use, and among the most expensive and time-consuming to develop and maintain. OS software must also be robust and dependable, since OS failures can result in system crashes that corrupt user data, endanger human lives (cf. embedded systems), or provide open avenues of attack for hackers or even cyber-terrorists.
References
[1]
R. Alur, R. Grosu, and M. McDougall. Efficient reachability analysis of hierarchical reactive machines. In Computer Aided Verification, 12th International Conference, LNCS 1855, pages 280--295. Springer, 2000.
[2]
T. Ball, R. Majumdar, T. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI 2001, SIGPLAN Notices 36(5), pages 203--213, 2001.
[3]
J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from java source code. In Proceedings of 22nd International Conference on Software Engineering, pages 439--448, 2000.
[4]
D. Engler, D. Y. Chen, S. Hallem, A. Chou, and B. Chelf. Bugs as Deviant Behavior: A General Approach to Inferring Errors in Systems Code. In Proceedings of the 18th ACM Symposium on Operating System Principles (SOSP 2001), Chateau Lake Louise, Banff, Canada, October 2001. ACM SIGOPS.
[5]
R. Grosu, Y. A. Liu, S. A. Smolka, S. D. Stoller, and J. Yan. Automated software engineering using concurrent class machines. In Proceedings of ASE'01, the 16th IEEE International Conference on Automated Software Engineering. IEEE, 2001.
[6]
A. Kolawa and A. Hicken. Insure++: A Tool to Support Total Quality Software. http://www.parasoft.com/insure/papers/tech.htm, March 2001.
[7]
S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. ERASER: A Dynamic Data Race Detector for Multithreaded Programs. ACM Transactions on Computer Systems, 15(4):391--411, 1997.
[8]
A. Tevanian and C. Minshall. File System Exerciser. http://www.codemonkey.org.uk/cruft/fsx-linux.c, 1991.
- High-confidence operating systems
Recommendations
High-resolution side channels for untrusted operating systems
USENIX ATC '17: Proceedings of the 2017 USENIX Conference on Usenix Annual Technical ConferenceFeature-rich mass-market operating systems have large trusted computing bases (TCBs) and a long history of vulnerabilities. Systems like Overshadow, InkTag or Haven attempt to remove the operating system (OS) from the TCB of applications while retaining ...
Teaching operating systems: the windows case
An operating system (OS) is a program that manages computer hardware. And although today's commercial-off-the-shelf desktop operating systems appear to be an integral part of PCs and workstation to many users, a fundamental understanding of the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
July 2002
258 pages
Copyright © 2002 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 July 2002
Check for updates
Qualifiers
- Article
Acceptance Rates
Overall Acceptance Rate 37 of 37 submissions, 100%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 88Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 01 Mar 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in