Graduate Programs in the Life Sciences

Submitted or In Press

Device driver safety through a reference validation mechanism.  Accepted for publication, OSDI 2008.  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.

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.

Hyperproperties.  Proceedings 21st IEEE Computer Security Foundations Symposium (Pittsburgh, PA, June 2008), 51 -- 65.  Also available as Computing and Information Science Technical Report 1813/9480. January 2008.  With Michael R. Clarkson.