Data processing: software development – installation – and managem – Software program development tool – Translation of code
Patent
1997-10-28
2000-10-03
Hafiz, Taria R.
Data processing: software development, installation, and managem
Software program development tool
Translation of code
717 7, G06F 944
Patent
active
061287741
ABSTRACT:
A computer-implemented method of verifying that untrusted software supplied by a code producer is safe to execute by a code consumer. The method includes the step of defining a safety policy that specifies safe operating conditions of the untrusted software on the code consumer. The method also includes the steps of generating a safety predicate for the untrusted software that determines if execution by the code consumer of the untrusted software will violate said safety policy and generating a safety proof that proves that said safety predicate is valid. The method further includes the step of validating the untrusted software for execution based on said safety proof and said safety predicate.
REFERENCES:
patent: 5193180 (1993-03-01), Hastings
patent: 5590329 (1996-12-01), Goodnow, II
patent: 5596682 (1997-01-01), Yamazaki
patent: 5692047 (1997-11-01), McManis
patent: 5761477 (1998-06-01), Wahbe
patent: 5790778 (1998-08-01), Bush
patent: 5797128 (1997-05-01), Birnbaum
patent: 5854924 (1998-12-01), Rickel
patent: 5920716 (1996-11-01), Johnson et al.
patent: 5978484 (1996-04-01), Apperson et al.
patent: 5987252 (1997-09-01), Leino et al.
Necula, G. et al., "Efficient Representation and Validation of Logical Proofs", Technical Report CMU-CS-97-172, Computer Science Department, Carnegie Mellon University, Oct. 1997.
Detlefs, D., "An Overview of the Extended Static Checking System", Proceedings of the First Formal Methods in Software Practice Workshop 1996.
Harper, R. et al., "A Framework for Defining Logics", Journal of the Association for Computing Machinery 40, 1 (Jan. 1993), pp. 143-84.
Owre, S. et al., "A Prototype Verification System", 11.sup.th International Conference on Automated Deduction (CADE), Jun. 1992.
Pfenning, F., "Elf: A Language for Logic Definition and Verified Meta-Programming", Fourth Annual Symposium on Logic in Computer Science, Jun. 1989, IEEE Computer Society Press.
Constable, R., et al., "Implementing Mathematics with the Nuprl Proof Development System", Prentice Hall, 1986, pp. 1-17, 41-95 115-31.
Coquand, T., et al., "Constructions: A Higher Order Proof System for Mechanizing Mathematics", Proceedings of the European Conference on Computer Algebra (EU-ROCAL '85), LNCS 203, Apr. 1985, pp. 151-84.
Gordon, M., "HOL: A Machine Oriented Formulation of Higher Order Logic", Tech. Rep. 68, University of Cambridge, Computer Laboratory, Jul. 1985.
Boyer, R., et al., "A Computational Logic", Academic Press, 1979, pp. 1-55, 87-91, 253-81.
Luckham, D., et al., "Stanford Pascal Verifier User Manual", Tech. Rep. No. STAN-CS-79-73 1, Department of Computer Science, Stanford Univ., Mar. 1979.
Nelson, G., et al., "Simplification by Cooperating Decision Procedures", Tech. Rep. No. STAN-CS-78-652, Department of Computer Science, Stanford Univ., Apr. 1978.
Adl-Tabatabai, et al., "Efficient and Language-Independent Mobile Programs", School of Computer Science, Carnegie Mellon University, Oct. 1995.
Bershad, et al., "Extensibility, Safety and Performance in the SPIN Operating System", a version appeared in The Proceedings of the 15.sup.th Symposium on Operating Systems Principles, Department of Computer Science & Engineering, University of Washington.
Engler, et al., "DPF: Fast, Flexible Message Demultiplexing using Dynamic Code Generation", SIGCOMM '96, Aug. 1996.
Engler, et al., "The Operating System Kernel as a Secure Programmable Machine", M.I.T. Laboratory for Computer Science (Publication date unknown).
Hsieh, et al., "Language Support for Extensible Operating Systems", Department of Computer Science and Engineering, University of Washington (Publication date unknown).
IBM Corporation, "Mechanism for Trusted Computing Base Definition and Checking", IBM Technical Disclosure Bulletin, vol. 34, No. 9, pp. 188-191, Feb. 1992.
IBM Corporation, "Mechanism for Trusted Computing Base Isolation", IBM Technical Disclosure Bulletin, vol. 34, No. 8, pp. 214-215, Jan. 1992.
IBM Corporation, "One-Bit Branch Prediction for Processors with Fixed Prediction Mechanism", IBM Technical Disclosure Bulletin, vol. 38, No. 10, p. 217-218, Oct. 1995.
McCanne, et al., "The BSD Packet Filter: A New Architecture for User-level Packet Capture", 1993 Winter USENIX, Jan. 25-29, 1993, pp. 259-269.
Mogul, et al., "The Packet Filter: An Efficient Mechanism for User-level Network Code", Proceedings of the 11.sup.th Symposium on Operating Systems Principles, ACM SIGOPS, Austin, Texas, Nov. 1987.
Seltzer, et al., "Dealing With Disaster: Surviving Misbehaved Kernel Extensions", Proceedings of the Symposium on Operating System Principles, 1993.
Wahbe, et al., "Efficient Software-Based Fault Isolation", Proceedings of the Symposium on Operating System Principles, 1993.
Wallach, et al., "ASHs: Application-Specific Handlers for High-Performance Messaging", SIGCOMM '96, Aug. 1996.
George C. Necula, Proof-Carrying Code, Proc. of the 24th ACM SIGPLAN-SIGACT Symp'm on Principles of Programming Languages, 106-19, Jan. 1997.
Ravi Sethi, Programming Languages: Concepts and Constructs, 404, 448, 1989.
John C. Mitchell, Foundations for Programming Languages, 402, 693, 1996.
Edsger W. Dijkstra and Carel S. Scholten, Predicate Calculus and Program Semantics, 77, 139, 193, 1990.
Martin Davis, Computability and Unsolvability, 131, 1982.
George C. Necula and Peter Lee, Safe Kernel Extensions without Run-Time Checking [online], Sep. 17, 1996 [retrieved on Jul. 7, 1999]. Retrieved from URL:http://www.cs.cmu.edu/.about.petel/papers/pcc/osdi.
George C. Necula and Peter Lee, Safe Kernel Extensions without Run-time Checking, Jan. 1996.
Lee Peter
Necula George C.
Hafiz Taria R.
Pender, Jr. Michael J.
LandOfFree
Safe to execute verification of software does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Safe to execute verification of software, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Safe to execute verification of software will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-206149