Fred B. Schneider Publications


	Fred B. Schneider Publications Return to Fred B. Schneider Home Submitted or In Press Device driver safety through a reference validation mechanism. Submitted for publication. With Dan Williams, Patrick Reynolds, Kevin Walsh, and Emin Gun Sirer. Using external security monitors to secure BGP. Submitted for publication. With Patrick Reynolds, Oliver Kennedy, and Emin Gun Sirer. Independence from obfuscation: A semantic framework for diversity. Submitted for publication. (Extended version of a paper with the same title appearing in Proceedings 19th IEEE Computer Security Foundations Workshop.) With Riccardo Pucella. Trustworthiness as a limitation on network neutrality. Accepted for publication, Federal Communications Law Journal, Vol. 61. With Aaron Burstein. Hyperproperties. To appear, 21st IEEE Computer Security Foundations Symposium (Pittsburgh, PA, June 2008). Also available as Computing and Information Science Technical Report 1813/9480. January 2008. With Michael R. Clarkson. Belief in information flow. Invited paper. To appear, Journal of Computer Security. Available as Cornell Computer Science Department Technical Report TR 2007-2075, February 2005. With Michael R. Clarkson and Andrew C. Myers. Books A Logical Approach to Discrete Math. Springer-Verlag, NY, 1993, 500 pages. With David Gries. Instructor's Manual for "A Logical Approach to Discrete Math''. D. Gries and F. B. Schneider, Ithaca, NY, 1993. 311 pages. With David Gries. This is available to instructors for a nominal fee. Send email for instructions. On Concurrent Programming. Springer-Verlag, NY, 1997, 473 pages. Trust in Cyberspace. (F. B. Schneider, Editor) National Academy Press, December 1998, 331 pages. Journals Conditions for the equivalence of synchronous and asynchronous operation. IEEE Transactions on Software Engineering SE-4, 6 (November 1978), 507--516. With A. J. Bernstein, E. A. Akkoyunlu and A. Silbershatz. Master keys for group sharing. Information Processing Letters 12, 1 (February 1981), 23--25. With D. Denning. More on master keys for group sharing. Information Processing Letters 13, 3 (December 1981), 125--126. With D. Denning and H. Meijer. Synchronization in distributed programs. TOPLAS 4, 2 (April 1982), 125--148. [TR 79-391] Fail-stop processors: An approach to designing fault-tolerant computing systems. TOCS 1, 3 (August 1983), 222--238. With R. D. Schlichting. User recovery and reversal in interactive systems. TOPLAS 6, 1 (January 1984), 1--19. With J. Archer and R. W. Conway. [TR 81-476] The `Hoare Logic' of CSP and all that. TOPLAS 6, 2 (April 1984), 281--296. With L. Lamport. Fault-tolerant broadcasts. Science of Computer Programming 4, 1 (April 1984), 1--15. With D. Gries and R. D. Schlichting. Key exchange using `Keyless Cryptography'. Information Processing Letters 16, 2 (February 1983), 79--82. With B. Alpern. [TR 82-513] Concepts and notations for concurrent programming. ACM Computing Surveys 15, 1 (March 1983), 3--44. With G. Andrews. [TR 82-520] Using message-passing for distributed programming: Proof rules and disciplines. TOPLAS 6, 3 (July 1984), 402--431. With R. D. Schlichting. [TR 82-491] Byzantine generals in action: Implementing fail-stop processors. TOCS 2, 2 (May 1984), 145--154. [TR 83-569] Derivation of a distributed algorithm for finding paths in directed networks. Science of Computer Programming 6, 1 (January 1986), 1--9. With R. McCurley. [TR 83-586] Thrifty execution of task pipelines. Acta Informatica 22, 1 (1985), 35--45. With R. W. Conway and D. Skeen. [TR 84-615] Defining liveness. Information Processing Letters 21, 4 (October 1985), 181--185. With B. Alpern. [TR 85-650] Safety without stuttering. Information Processing Letters 23, 4 (November 1986), 177--180. With B. Alpern and A. J. Demers. [TR 85-708] Recognizing safety and liveness. Distributed Computing 2, 3 (1987), 117--126. With B. Alpern. [TR 86-727] Verifying temporal properties without temporal logic. TOPLAS 11, 1 (January 1989), 147--167. With B. Alpern. [TR 87-848] Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys 22, 4 (December 1990), 299--319. [TR 86-800] Trace-based network proof systems: Expressiveness and completeness. TOPLAS 14, 3 (July 1992), 396--416. With J. Widom and D. Gries. [TR 89-966] Preserving liveness: Comments on "Safety and Liveness from a Methodological Point of View''. Information Processing Letters 40, 3 (November 1991), 141--142. With M. Abadi, B. Alpern, K. R. Apt, N. Francez, S. Katz, and L. Lamport. A formalization of priority inversion. Real Time Systems 5 (1993), 285--303. With O. Babaoglu and K. Marzullo. [TR 90-1088] Proving nondeterministically specified safety properties using progress measures. Information and Computation 107, 3 (November 1993), 151--170. With N. Klarlund. [TR 90-1167] A new approach to teaching discrete mathematics. Primus V 2 (June 1995), 113--138. With D. Gries. [TR 94-1411] Teaching math more effectively, through the design of calculational proofs. The Mathematical Monthly (October 1995), 691--697. With D. Gries. [TR 94-1415] Equational Propositional Logic. Information Processing Letters 53, 3 (February 1995), 145--152. With D. Gries. [TR 94-1455] Verifying Programs that use Causally-ordered Message-passing. Science of Computer Programming 24, 2 (1995), 105--128. With S. Stoller. [TR 94-1423] Hypervisor-based Fault-Tolerance. ACM Transactions on Computer Systems 14, 1 (February 1996), 80--107. With T. Bressoud. [TR 95-1495] Adding the everywhere operator to propositional logic. Journal of Logic and Computation 8, 1 (February 1998), 119--129. With D. Gries. [TR 96-1583] Building trustworthy systems: Lessons from the PTN and Internet. IEEE Internet Computing 3, 5 (November-December 1999), 64--72. With S. Bellovin and A. Inouye. Enforceable security policies. ACM Transactions on Information and System Security 3, 1 (February 2000), 30--50. [TR 99-1759] A Tacoma Retrospective. Software--Practice and Experience 32, 605--619. With Dag Johansen, Kare Lauvset, Robbert van Renesse, Nils Sudmann, and Kjetil Jacobsen. COCA: A secure distributed on-line certification authority. ACM Transactions on Computer Systems 20, 4 (November 2002), 329--368. With Lidong Zhou and Robbert van Renesse. Earlier version: Technical Report TR 2000-1828, December 7, 2000. Tolerating Malicious Gossip. Distributed Computing 16, 1 (February 2003), 49--68. With Yaron Minsky. Least Privilege and More. IEEE Security and Privacy, Volume 1, Number 3 (September/October 2003), 55--59. This is a revised version of Least Privilege and More, in Computer Systems: Papers for Roger Needham. Andrew Herbert and Karen Sparck Jones, eds., Springer-Verlag, New York, 253--258. CODEX: A robust and secure secret distribution system. IEEE Transactions on Dependable and Secure Computing, Vol 1, No. 1 (January-March 2004), 34--47. With Michael Marsh. Automated analysis of fault-tolerance in distributed systems. Formal Methods in System Design, Volume 26, Number 2 (March 2005), 183--196. With Scott Stoller. Earlier version is available here. APSS: Proactive secret sharing in asynchronous systems. ACM Transactions on Information and System Security 8, 3 (August 2005), 259--286. Earlier version available as Cornell Computer Science Department Technical Report TR 2002-1877, October 2002. With Lidong Zhou and Robbert van Renesse. Implementing trustworthy services using replicated state machines. IEEE Security and Privacy, Volume 3, Number 5 (September/October 2005), 34--43. Earlier version available as Cornell Computer Science Department Technical Report TR 2004-1924, January 2004. With Lidong Zhou. Computability classes for enforcement mechanisms. ACM TOPLAS, 28, 1 (Januray 2006), 175--205. Also available as Cornell Computer Science Department Technical Report TR 2003-1908, August 2003. With Kevin W. Hamlen and Greg Morrisett. Conference Proceedings On language restrictions to ensure deterministic behavior in concurrent systems. Proc. of Third Jerusalem Conference on Information Technology (Jerusalem, Israel, August 1978), North-Holland, New York, 537--541. With A. J. Bernstein. [TR 79-374] Ensuring consistency in a distributed database system by use of distributed semaphores. Proc. International Symposium on Distributed Databases (Paris, France, March 1980), North-Holland, New York, 183-189. [TR 79-392] The master key problem. Proc. 1980 Symposium on Security and Privacy (Oakland, California, April 1980), IEEE Computer Society, Oakland, California, 103--107. With D. Denning. [TR 80-409] Towards fault tolerant process control software. Proc. of 1981 International Symposium on Fault-Tolerant Computing (Portland, Maine, June 1981), IEEE Computer Society, Oakland, California, 48--55. With R. D. Schlichting. Understanding and using asynchronous message-passing primitives. Proc. of ACM Symposium on Principles of Distributed Computing (Ottawa, Canada, August 1982), ACM, New York, 141--147. With R. D. Schlichting. Fail-Stop processors. (Invited Paper.) Digest of Papers Spring Compcon '83 (San Francisco, California, March 1983), IEEE Computer Society, Oakland, California, 66--71. Declarations: A uniform approach to aliasing and typing. Proc. of 12th Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (New Orleans, Louisiana, January 1985), ACM, New York, 205--216. With L. Lamport. [TR 84-635] Inexact agreement: Accuracy, precision, and graceful degradation. Proc. Fourth Annual SIGACT-SIGOPS Symposium on Principles of Distributed Computing (Minaki, Ontario, Canada, August 1985), ACM, New York, 237--249. With S. R. Mahaney. Symmetry and Similarity in Distributed Systems. Proc. Fourth Annual SIGACT-SIGOPS Symposium on Principles of Distributed Computing (Minaki, Ontario, Canada, August 1985), ACM, New York, 13--22. With R. E. Johnson. [TR 85-677] Abstractions for fault-tolerance in distributed systems. (Invited Paper.) Proc. IFIP 10th World Computer Congress, IFIP '86 (Dublin, Ireland, September 1986), 727--733. A paradigm for reliable clock synchronization. (Invited paper.) Proc. Advanced Seminar on Real-Time Local Area Networks (Bandol, France, April 1986), INRIA, 85--104. Completeness and incompleteness of trace-based network proof systems. Proc. of 14th Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Munich, F. R. Germany, January 1987), 27--38. With J. Widom and D. Gries. Proving Boolean combinations of deterministic properties. Proc. of 2nd Annual Symposium on Logic in Computer Science (Ithaca, New York, June 1987), 131--137. With B. Alpern. Primary-Backup Protocols: Lower Bounds and Optimal Protocols. Proc. 3rd IFIP Working Conference on Dependable Computing for Critical Applications (Sicily, Italy, September 1992), 187--196. With Navin Budhiraja, Keith Marzullo and Sam Toueg. [TR 92-1265] Optimal primary-backup protocols. Proc. 6th International Workshop, WDAG '92 (Haifa, Israel, November 1992), Lecture Notes in Computer Science, Volume 647, Springer-Verlag, New York, 1992, 362--378. With Navin Budhiraja, Keith Marzullo and Sam Toueg. Reasoning about Programs by exploiting the environment. Proc. 21st International Colloquium, ICALP '94 (Jerusalem, Israel, July 1994), Lecture Notes in Computer Science, Volume 820, Springer-Verlag, New York, 328--339. With L. Fix. Hybrid verification by exploiting the environment. Formal Techniques in Real Time and Fault Tolerant Systems (Luebeck, Germany, September 1994), Lecture Notes in Computer Science, Volume 863, Springer-Verlag, New York, 1--18. With Limor Fix. Teaching logic as a tool. Proc. 26th SIGCSE Technical Symposium on Computer Science Education (Nashville, Tennessee, March 1995), SIGCSE Bulletin 27, 1, 384--385. With D. Gries. Operating system support for mobile agents. Proc. Fifth Workshop on Hot Topics in Operating Systems (HOTOS-V) (Orcas Island, Washington, May 1995), 42--45. With Dag Johansen and Robbert van Renesse. Faster possibility detection by combining two approaches. Proc. 9th International Workshop, WDAG '95 (Le Mont-Saint-Michel, France, September 1995), Lecture Notes in Computer Science, Volume 972, Springer-Verlag, New York, 1995, 318--332. With Scott Stoller. Hypervisor-based Fault Tolerance. Proc. Fifteenth ACM Symposium on Operating Systems Principles (Copper Mountain Resort, Colorado, December 1995), Operating Systems Review 29, 5, 1--11. With T. Bressoud. Cryptographic support for fault-tolerant distributed computing. Proc. of the Seventh ACM SIGOPS European Workshop "System Support for Worldwide Applications'' (Connemara, Ireland, September 1996), ACM, New York, 109--114. With Yaron Minsky, Robbert van Renesse, and Scott D. Stoller. Supporting broad internet access to TACOMA. Proc. of the Seventh ACM SIGOPS European Workshop "System Support for Worldwide Applications'' (Connemara, Ireland, September 1996), ACM, New York, 55--58. With Dag Johansen and Robbert van Renesse. Automated analysis of fault-tolerance in distributed systems. Proc. of the First ACM SIGPLAN Workshop on Automated Analysis of Software (Paris, France, January 1997), ACM, New York, 33--44. Rance Cleaveland and Daniel Jackson, (eds.). With Scott Stoller. Towards fault-tolerant and secure agentry. Proc. 11th International Workshop WDAG '97 (Saarbrucken, Germany, September 1997), Lecture Notes in Computer Science, Volume 1320, Springer-Verlag, Heidelberg, 1997, 1--14. Automated stream-based analysis of fault-tolerance. Formal Techniques in Real-time and Fault-Tolerant Systems (FTRTFT '98) (Lyngby, Denmark, September 1998), Lecture Notes in Computer Science, Volume 1486, Springer-Verlag, Berlin, 1998, 113--122. With Scott Stoller. NAP: Practical Fault-tolerance for Itinerant Computations. Proc. 19th IEEE International Conference on Distributed Computing Systems (Austin, Texas, June 1999), IEEE, 180--189. With D. Johansen, K. Marzullo, K. Jacobsen, and D. Zagorodnov. SASI enforcement of security policies: A retrospective. Proceedings of the New Security Paradigms Workshop (Caledon Hills, Ontario, Canada, September 1999), Association for Computing Machinery, 87--95. With Ulfar Erlingsson. IRM enforcement of Java stack inspection. Proceedings 2000 IEEE Symposium on Security and Privacy (Oakland, California, May 2000), IEEE Computer Society, Los Alamitos, California, 246--255. With Ulfar Erlingsson. [TR 2000-1786] Open source in security: Visiting the bizarre. Proceedings 2000 IEEE Symposium on Security and Privacy (Oakland, California, May 2000), IEEE Computer Society, Los Alamitos, California, 126--127. A language-based approach to security. Informatics: 10 Years Back, 10 Years Ahead (Saarbrucken, Germany, August 2000), Lecture Notes in Computer Science, Volume 2000 (Reihnard Wilhelm, ed.), Springer-Verlag, Heidelberg, 2000, 86-101. And Greg Morrisett, Robert Harper. Chain Replication for Supporting High Throughput and Availability (.pdf, .html). Sixth Symposium on Operating Systems Design and Implementation (OSDI '04). USENIX Association, (San Francisco, California, December 2004), 91--104. With Robbert van Renesse. Peer-to-Peer authentication with a distributed single sign-on service. Peer-to-Peer Systems III, Third International Workshop IPTPS 2204 (La Jolla, CA, February 2004), Lecture Notes in Computer Science, Volume 3279 (G. Voelker and S. Shenker, eds.), Springer-Verlag, Heidelberg, 2004, 250--258. Preliminary version available as Cornell Computer Science Department Technical Report TR 2004-1930, February 2004. With William Josephson and Emin Gun Sirer. Distributed blinding for distributed ElGamal re-encryption. Proceedings 25th IEEE International Conference on Distributed Computing Systems (Columbus, Ohio, June 2005), 815--824. Earlier version available as Cornell Computer Science Department Technical Report TR 2004-1920, January 2004. With Lidong Zhou, Michael A. Marsh, and Anna Redz. Belief in information flow. Proceedings 18th IEEE Computer Security Foundations Workshop (Aix-en-Provence, France, June 20-22, 2005), 31--45. Earlier version available as Cornell Computer Science Department Technical Report TR 2005-1976, February 2005. With Michael R. Clarkson and Andrew C. Myers. Certified in-lined reference monitoring on .NET. Proceedings of the 2006 Programming Languages and Analysis for Security Workshop (Ottawa, Ontario, Canada, June 10, 2006), ACM, 2006, 7--16. Extended version available as Cornell University Computer Science Department Technical Report TR 2005-2003. With Kevin Hamlen and Greg Morrisett. Independence from obfuscation: A semantic framework for diversity. Proceedings 19th IEEE Computer Security Foundations Workshop (Venice, Italy), July 2006, 230--241. Expanded version available as Cornell University Computer Science Department Technical Report TR 2006-2016. January 2006. With Riccardo Pucella. Network security and the need to consider provider coordination in network access policy. Presented at 35th Research Conference on Communication, Information and Internet Policy (TPRC), (Arlington, Virginia, Sept. 2007). With Aaron Burstein. The building blocks of consensus. Proceedings 9th International Conference on Distributed Computing and Networking, ICDCN 08, (Kolkata, India, Jan. 2008), Lecture Notes in Computer Science, Volume 4904 (S. Rao et al, eds.), Springer-Verlag, Heidelberg, 2008, 54--72. With Yee Jiun Song, Robert van Renesse, and Danny Dolev. Other Publications Scheduling in Concurrent Pascal. Operating Systems Review 12, 2 (April 1978), 15--21. With A. J. Bernstein. [TR 79-365] Synchronization and concurrent programming. Handbook of Electrical and Computer Engineering, John Wiley and Sons, 1983. [TR 80-425] Abstract data types. Handbook of Electrical and Computer Engineering, John Wiley and Sons, 1983. Broadcasts: A paradigm for distributed programs. Proc. Workshop on Fundamental Issues in Distributed Computing (Fallbrook, California, December 1980), ACM, New York. [TR 80-440] Book review: The Practical Guide to Structured Systems Design. IEEE Spectrum 18, 3 (March 1981), 92. The fail-stop processor approach. Invited chapter in Reliability in Distributed Software and Database Systems (B. Bhargava, ed.), Von Nostrand Reinhold Company, New York, 1987, 370--394. Distributed Systems---Methods and Tools for Specification. Lecture Notes in Computer Science, Volume 190, Springer-Verlag, New York, 1985. With M. W. Alford, J. P. Ansart, G. Hommel, L. Lamport, and B. Liskov. A reply to "A Review of the Advanced Course Description in Computer Science of the Educational Testing Service''. Contemporary Education Review 2, 3. With P. Miller, T. Gill, S. Owicki, B. Presley, and J. Wadkins. Reaching agreement: A fundamental task even in distributed computer systems. Engineering: Cornell Quarterly 20, 2 (Fall 1985), 18--22. And O. Babaoglu, K. P. Birman, and S. Toueg. Programming methodology: Making a science out of an art. Engineering: Cornell Quarterly 20, 2 (Fall 1985), 23--27. With D. Gries. Concepts for concurrent programming. (Invited Paper.) Current Trends in Concurrency, (J. W. de Bakker, W. P. de Roever, and G. Rozenberg, eds.), Lecture Notes in Computer Science, Volume 224, Springer-Verlag, New York, 1986, 669--716. And G. Andrews. The state machine approach: A tutorial. (Invited paper.) Proc. Workshop on Fault-tolerant Distributed Computing, (B. Simons and A. Z. Spector, eds.) Lecture Notes in Computer Science, Volume 448, Springer-Verlag, New York, 1990, 18--41. Another position paper on "fairness''. Software Engineering Notes 13, 3 (July 1988), 18--19. With L. Lamport. Critical (of) issues in real-time systems: A position paper. (Invited paper.) Real-time systems Newsletter 4, 2 (Summer 1988), 3--5. Also reprinted in Distributed Processing Technical Committee Newsletter 10, 2 (November 1988), 75--77. Cornell's real-time reliable (RR) systems project. Proc. Foundations of Real-time Computing, Office of Naval Research Research Initiative Kickoff Workshop, 28--32. Computer Systems. Computer Science: Achievements and Opportunities, SIAM Reports on Issues in the Mathematical Sciences, SIAM, Philadelphia, Pennsylvania, 1989, 29--40. With F. Baskett, D. Clark, A. N. Habermann, B. Liskov, and B. Smith. Formal verification of concurrent software. Proc. of Thirteenth Annual International Computer Software and Applications Conference (Orlando, Florida, September 1989), 59. Simpler proofs for concurrent reading and writing. Beauty is Our Business, Springer-Verlag Texts and Monographs in Computer Science, May 1990, 373--389. [TR 89-1037] Towards derivation of real-time process-control programs. Proc. of Third Annual Workshop, Foundations of Real-time Computing Initiative (Washington, DC, October 1990), Office of Naval Research, 373--384. With K. Marzullo. Derivation of sequential, real-time process-control programs. Foundations of Real-Time Computing: Formal Specifications and Methods, (A. M. van Tilborg and G. Koob, eds.), Kluwer Academic Publishers, 1991, 39--54. With K. Marzullo and N. Budhiraja. [TR 91-1217] Fault-tolerance support in distributed systems workshop. ESN Information Bulletin 91-03 (July 1991), Office of Naval Research European Office, 58--59. The challenge is usability. 2021 AD: Visions of the Future, National Engineering Consortium, 1991, 50. Putting time into proof outlines. Proc. of the REX Workshop "Real-Time: Theory in Practice'', (J. W. de Bakker, C. Huizing, W. P. de Roever, G. Rozenberg, eds.), Lecture Notes in Computer Science, Volume 600, Springer-Verlag, Berlin, 1991, 618--639. And Bard Bloom and Keith Marzullo. [TR 91-1238] Reasoning about real-time actions. Proc. of Fourth Annual Workshop, Foundations of Real-time Computing Initiative, (Washington, DC, October 1991), Office of Naval Research, 85--91. And Bard Bloom and Keith Marzullo. Lower bounds for primary-backup implementations of BOFO services. Proc. of Second Annual Workshop, Ultradependable Multicomputers and Electronic Systems (Washington, DC, November 1991), Office of Naval Research, 81--86. With Navin Budhiraja, Keith Marzullo, and Sam Toueg. Assertional methods for fault-tolerant, real-time concurrent programs. Proc. Software Technology Conference 1992 (Los Angeles, California, April 1992) Defense Advanced Research Projects Agency, Software and Intelligent Systems Technology Office and Computing Systems Technology Office, 516--517. Introduction. Distributed Computing 6, 1 (June 1992), 1--3. Adding fault-tolerance, virtually. Proc. of First Annual Workshop on Embedded Systems (Austin, Texas, January 1993), Office of Naval Research, 41. What good are models and what models are good? Chapter 2, Distributed Systems, 2nd Edition (S. Mullender, ed.), Addison Wesley, 1993, 17--25. Replication management using the state machine approach. Chapter 7, Distributed Systems, 2nd Edition (S. Mullender, ed.), Addison Wesley, 1993, 169--195. The primary-backup approach. Chapter 8, Distributed Systems, 2nd Edition (S. Mullender, ed.), Addison Wesley, 1993, 199--215. With Navin Budhiraja, Keith Marzullo, and Sam Toueg. A role for formal methodists. Fourth International Workshop on Dependable Computing for Critical Applications (San Diego, California, January 1994), 29--30. Research on fault-tolerant and real-time computing. Software and Systems Program Summary. (Bolling Air Force Base, Washington, DC, September 1994), Air Force Office of Scientific Research, 75--77. Refinement for Fault-Tolerance: An Aircraft Hand-off Protocol. Foundations of Ultradependable Parallel and Distributed Computing, Paradigms for Dependable Application, Kluwer Academic Publishers, 1994, 39--54. With K. Marzullo and J. Dehn. [TR 94-1417] On teaching proof. Arts & Sciences NewsLetter 16, 2 (Spring 1995), 3. With D. Gries. Avoiding AAS Mistakes. (Invited paper.) Proc. of the Air Traffic Management Workshop, (L. Tobais, M. Tashker, A. Boyle, eds.), NASA Conference Publication 10151, NASA Ames Research Center, February 1995, 133--149. Avoiding the undefined by underspecification. Computer Science Today Recent Trends and Developments (Jan van Leeuwen, ed.), Lecture Notes in Computer Science, Volume 1000, Springer-Verlag, 1995, 366--373. With David Gries. On Traditions in Marktoberdorf. Deductive Program Design (M. Broy, ed.), ASI Volume F152. Springer-Verlag, Heidelberg, 1--4. Notes on Proof Outline Logic. Deductive Program Design (M. Broy, ed.), ASI Volume F152. Springer-Verlag, Heidelberg, 351--394. Report on Dagstuhl Seminar on Time Services, Schloss Dagstuhl, March 11--March 15 1996. Real-Time Systems 12, 3 (May 1997), 329--345. With Danny Dolev, Rudiger Reischuk, and H. Raymond Strong. Editorial: New Partnership with ACM. Distributed Computing 10, 2 (1997), 63. On Concurrent Programming. Invited "Inside Risks" column. Communications of the ACM 41, 4 (April 1998), 128. Improving Networked Information System Trustworthiness: A Research Agenda. Proceedings 21st National Information Systems Security Conference(October 1998, Arlington, Virginia), National Computer Security Center, 766. Toward Trustworthy Networked Information Systems. Invited "Inside Risks'' column. Communications of the ACM 41, 11 (November 1998), 144. Evolving Telephone Networks. Invited "Inside Risks'' column. Communications of the ACM 42, 1 (January 1999), 160. With S. Bellovin. What Tacoma Taught Us. Mobility: Processes, Computers, and Agents, Dejan S. Milojicic, Frederick Douglis, and Richard G. Wheeler (eds.), Addison Wesley and the ACM Press, April 1999, 564--566. With Dag Johansen and Robbert van Renesse. Fred B. Schneider on Distributed Computing. Interview by Dejan Milojicic, Distributed Systems Online 1, 1 (2001) . Formalizations of substitutions of equals for equals. Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford-Microsoft Symposium in honour of Professor Sir Antony Hoare, (Davies, Roscoe, and Woodcock eds.) Palgrave Publishers, Hampshire, England, November 2000, 119--132. With David Gries. [TR 98-1686] Secure Systems Conundrum. Invited "Inside Risks'' column. Communications of the ACM 45, 10 (October 2002), 160. WAIF: Web of Asynchronous Filters. Future Directions in Distributed Computing, Lecture Notes in Computer Science, Volume 2584, Springer-Verlag, Heidelberg, 2003, 81--86. With Dag Johansen and Robbert van Renesse. Lifting reference monitors from the kernel. Formal Aspects of Security, FASec 2002 (London, United Kingdom, December 2002), Ali E. Abdullah, Peter Ryan, and Steve Schneider (eds.). Lecture Notes in Computer Science, Volume 2629, Springer-Verlag, New York, 2003, 1--2. The Next Digital Divide. Editorial. IEEE Security & Privacy 2, 1 (January/February 2004), 5. Time Out for Station Identification. Editorial. IEEE Security & Privacy 2, 1 (September/October 2004), 5. Nexus: A new operating system for trustworthy computing. Work in Progress Session, 20th Symposium on Operating System Principles. October 2005, With Alan Shieh, Dan Williams, and Emin Gun Sirer. It Depends on What you Pay. Editorial. IEEE Security & Privacy 3, 3 (May/June 2005), 3. Here be Dragons. Editorial. IEEE Security & Privacy 3, 3 (May/June 2006), 3. Trusted Computing in Context. Editorial. IEEE Security & Privacy 5, 2 (March/April 2007), 4--5. Language-Based Security for Malicious Mobile Code. Department of Defense Sponsored Information Security Research: New Methods for Protecting Against Cyber Threats. Wiley Publishing Company, Indianapolis, Indiana, 2007, 477--494. With Dexter Kozen, Greg Morrisett, and Andrew C. Myers. Credentials-Based Authorization: Evaluation and Implementation. Abstract of Plenary Lecture. Proceedings 34th International Colloquium, ICALP 2007 (Wroclaw, Poland, July 2007), Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki (eds.). Lecture Notes in Computer Science, Volume 4596, Springer-Verlag, Heidelberg, 2007, 12--14. Mapping the Security Landscape: A Role for Language Techniques. Abstract of Invited Lecture. Proceedings 18th International Conference, CONCUR 2007 (Lisbon, Portugal, September 2007), Luis Caires and Vasco T. Vasconcelos (eds.). Lecture Notes in Computer Science, Volume 4703, Springer-Verlag, Heidelberg, 2007, 1. Unpublished Tech Reports Mechanisms for Specifying Scheduling Policies. Cornell University Computer Science Department Technical Report TR 79-365, January 1979. With A. J. Bernstein. On Restrictions to Ensure Reproducible Behavior in Concurrent Programs. Cornell University Computer Science Department Technical Report TR 79-374, 1979. With A. J. Bernstein. Personal Keys, Group Keys and Master Keys. Cornell University Computer Science Department Technical Report TR 80-409, 1980. With Dorothy E. Denning. Three Surveys on Operating System Topics. Cornell University Computer Science Department Technical Report TR 80-425, May 1980. With Gregory R. Andrews. Detecting Distributed Termination When Processors can Fail. Cornell University Computer Science Department Technical Report TR 80-449, December 1980. With G. W. Lerman. Cornell Local Network (CLONE) Interface Unit Principles of Operation. Cornell University Computer Science Department Technical Report TR 81-461, May 1981. An Approach to Designing Fault-Tolerant Computing Systems. Cornell University Computer Science Department Technical Report TR 81-479, November 1981. With Richard Schlichting. A Distributed Path Algorithm and its Correctness Proof. Cornell University Computer Science Department Technical Report TR 83-556, June 1983. With David D. Wright. Documentation for the CHIP Computer System. Cornell University Computer Science Department Technical Report TR 83-584, December 1983. With Ozalp Babaoglu, Mimi Bussan, Rogerio Drummond. Constraints: A Uniform Approach to Aliasing and Typing. Cornell University Computer Science Department Technical Report TR 84-635, September 1984. With Leslie Lamport. The HOCA Operating System Specifications. Cornell University Computer Science Department Technical Report TR 83-585, December 1983. With Ozalp Babaoglu. Understanding Protocols for Byzantine Clock Synchronization. Cornell University Computer Science Department Technical Report TR 87-859, August 1987. Decomposing Properties into Safety and Liveness using Predicate Logic. Cornell University Computer Science Department Technical Report TR 87-874, October 1987. Pretending Atomicity. Digital Equipment Corporation Systems Research Center Research Report 44, May 1989. Verifying Safety Properties Using Non-deterministic Infinite-star Automata. Cornell University Computer Science Department Technical Report TR 89-1036, September 1989. With Nils Klarlund. An Assertional Characterization of Serializability. Cornell University Computer Science Department Technical Report TR 89-1039, September 1989. With E. Robert McCurley. Priority Inversion and Its Prevention. Cornell University Computer Science Department Technical Report TR 90-1088, February 1990. With Ozalp Babaoglu, Keith Marzullo. Progress Measures for Verification Involving Non- determinism. Cornell University Computer Science Department Technical Report TR 90-1167, November 1990. With Nils Klarlund. The Trainset Railroad Simulation. Cornell University Computer Science Department Technical Report TR 93-1329, February 1993. With Richard Brown, Jacob Aizikowitz, Thomas C. Bressoud, Tony Lekas. Putting Time Into Proof Outlines. Cornell University Computer Science Department Technical Report TR 93-1333, March 1993. With Bard Bloom, Keith Marzullo. A Graphical Interface for CHIP. Cornell University Computer Science Department Technical Report TR 96-1591, June 1996, With Lorenzo Alvisi. Critical Infrastructures You Can Trust: Where Telecommunications Fits. Cornell University Computer Science Department Technical Report TR 98-1717, October 1998. With Steven Bellovin, Alan Inouye.