Fred B. Schneider Publications         Return to Fred B. Schneider Home


Work in Progress

The CloudProxy Tao for Trusted Computing.  Preliminary version available as University of California, Berkeley Technical Report No, UCB/EECS-2013-135, July 2013.  With John Manferdelli and Tom Roeder.

Draft chapters for a textbook on cybersecurity (as yet, untitled):

Introduction (2007);   Authenticating People (2009);    Discretionary Access Control (2012);    Mandatory Access Control (3/31/2014).    Credentials-based Authorization (4/15/2014).

Comments are welcome---none of these drafts is in final form.

Submitted or In Press

Vive La Difference:  Paxos vs. Viewstamped Replication vs. Zab.  Submitted for publication, October 2013.  With Robbert van Renesse and Nicolas Schiper.

Quantification of Integrity.  Accepted for publication.  Also available as Cornell Computing and Information Science Technical Report, January 12, 2011. With Michael R. Clarkson.

 

Writings on Science Policy

CALEA II:  Risks of Wiretap Modifications to Endoints.  White Paper, Center for Democracy & Technology.  With Ben Adida, Colin Anderson, Annie I. Anton, Roger Dingledine, Edward W. Felten, Matthew D. Green, J. Alex Halderman, David R. Jefferson, Cullen Jennings, Susan Landau, Navoop Mitter, Peter G. Neumann, Eric Rescorla, Bruce Schneier, Hovav Shacham, Micah Sherr, David Wagner, and Philip Zimmermann.

Blueprint for a Science of CybersecurityThe Next Wave.  Vol 19, No. 2 (2012), 47---57. Preliminary version available as Cornell Computing and Information Science Technical Report, May 2011.

Doctrine for CybersecurityDaedalus. Fall 2011, 70--92.  Also available as Cornell Computing and Information Science Technical Report, April 2011.  With Deirdre Mulligan.

Testimony.  United States House of Representatives Armed Services Committee, Terrorism, Unconventional Threats, and Capabilities Subcommitee, hearing February 25, 2010 on Private Sector Perspectives on Department of Defense Information Technology and Cybersecurity Activities.

Trustworthiness as a limitation on network neutralityFederal Communications Law Journal, Vol. 61 (2009), 591--623  With Aaron Burstein.


Testimony.  United States House of Representatives Committee on Science and Technology, Technology and Innovation Subcommittee, hearing October 22, 2009 on Cybersecurity Activities at NIST's Information Technology Laboratory .

Testimony.  United States House of Representatives Committee on Science and Technology, Research and Science Education Subcommittee, hearing June 10, 2009 on Cybersecurity R & D.

Notes for White House 60-day Cyber-Policy Review.  E. Lazowska and F.B. Schneider (eds), NSF submission for Cyberspace Policy Review conducted Spring 2009 for the White House.


Security is not a commodity:  The road forward for cybersecurity research. (.pdf, .doc).  Computing Research Initiatives for the 21st Century, Computing Community Consortium.  February 2009.  With Stefan Savage.

Toward a Safer and More Secure Cyberspace. S Goodman and H. Lin (eds), National Academies Press, Washington, DC, 2007, 328 pages.


Trust in Cyberspace. (F. B. Schneider, Editor) National Academy Press, Washington, DC, December 1998, 331 pages.

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. Preliminary version available as SUNY Stony Brook Department of Computer Science Technical Report -#60, January 1977.
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. Earlier version available as Cornell University Department of Computer Science Technical Report TR 79-391(scanned .pdf), September 1979.

Fail-stop processors: An approach to designing fault-tolerant computing systems. TOCS 1, 3 (August 1983), 222--238. Earlier version available as Cornell University Department of Computer Science Technical Report TR 81-479 (scanned .pdf), November 1981.With R. D. Schlichting.

User recovery and reversal in interactive systems. TOPLAS 6, 1 (January 1984), 1--19. Earlier version available as Cornell University Department of Computer Science Technical Report TR 81-476 (scanned .pdf), October 1981.With J. Archer and R. W. Conway.

The `Hoare Logic' of CSP and all that. TOPLAS 6, 2 (April 1984), 281--296. Earlier version available as Cornell University Department of Computer Science Technical Report TR 82-490, May 1982. With L. Lamport.

Fault-tolerant broadcasts. Science of Computer Programming 4, 1 (April 1984), 1--15. Earlier version available as Cornell University Department of Computer Science Technical Report TR 82-519, September 1982. With D. Gries and R. D. Schlichting.

Key exchange using `Keyless Cryptography'. Information Processing Letters 16, 2 (February 1983), 79--82. Earlier version available as Cornell University Department of Computer Science Technical Report TR 82-513, August 1982. With B. Alpern.

Concepts and notations for concurrent programming. ACM Computing Surveys 15, 1 (March 1983), 3--44. Earlier version available as Cornell University Department of Computer Science Technical Report TR 82-520 (scanned .pdf). With G. Andrews.

Using message-passing for distributed programming: Proof rules and disciplines. TOPLAS 6, 3 (July 1984), 402--431. Earlier version available as Cornell University Department of Computer Science Technical Report TR 82-491 (scanned .pdf), May 1982. With R. D. Schlichting.

Byzantine generals in action: Implementing fail-stop processors. TOCS 2, 2 (May 1984), 145--154. Earlier version available as Cornell University Department of Computer Science Technical Report TR 83-569 (scanned .pdf), August 1983.

Derivation of a distributed algorithm for finding paths in directed networks. Science of Computer Programming 6, 1 (January 1986), 1--9. Earlier version available as Cornell University Department of Computer Science Technical Report TR 83-586 (scanned .pdf), December 1983. With R. McCurley.

Thrifty execution of task pipelines. Acta Informatica 22, 1 (1985), 35--45. Earlier version available as Cornell University Department of Computer Science Technical Report TR 84-615 (scanned .pdf), June 1984. With R. W. Conway and D. Skeen.

Defining liveness.  Information Processing Letters 21, 4 (October 1985), 181--185. Earlier version available as Cornell University Department of Computer Science Technical Report TR 85-650 (scanned .pdf), October 1984. With B. Alpern.

Safety without stuttering. Information Processing Letters 23, 4 (November 1986), 177--180. Earlier version available as Cornell University Department of Computer Science Technical Report TR 85-708 (scanned .pdf) October 1985. With B. Alpern and A. J. Demers.

Recognizing safety and liveness.
Distributed Computing 2, 3 (1987), 117--126. Earlier version available as Cornell University Department of Computer Science Technical Report TR 86-727 (scanned .pdf), January 1986. With B. Alpern.
 
Verifying temporal properties without temporal logic. TOPLAS 11, 1 (January 1989), 147--167. Earlier version available as Cornell University Department of Computer Science Technical Report TR 87-848 (scanned .pdf), July 1987. With B. Alpern.

Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys 22, 4 (December 1990), 299--319. Earlier version available as Cornell University Department of Computer Science Technical Report TR 86-800 (scanned .pdf), December 1986.

Trace-based network proof systems: Expressiveness and completeness. TOPLAS 14, 3 (July 1992), 396--416. Earlier version available as Cornell University Department of Computer Science Technical Report TR 89-966 (scanned .pdf), February 1989. With J. Widom and D. Gries.

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, 4(1993), 285--303. Earlier version available as Cornell University Department of Computer Science Technical Report TR 90-1088 (scanned .pdf), February 1990. With O. Babaoglu and K. Marzullo.

Proving nondeterministically specified safety properties using progress measures. Information and Computation 107, 3 (November 1993), 151--170. Earlier versions available as Cornell University Department of Computer Science Technical Reports TR 90-1167 (scanned .pdf) and TR 91-1204 (scanned .pdf). With N. Klarlund .

A new approach to teaching discrete mathematics. (.pdf) Primus V 2 (June 1995), 113--138. Earlier version available as Cornell University Department of Computer Science Technical Report TR 94-1411 (scanned .pdf), February 1994. With D. Gries.

Teaching math more effectively, through the design of calculational proofs. The Mathematical Monthly (October 1995), 691--697. Earlier version available as Cornell University Department of Computer Science Technical Report TR 94-1415 (scanned .pdf), March 1994. With D. Gries.

Equational Propositional Logic. Information Processing Letters 53, 3 (February 1995), 145--152. Earlier version available as Cornell University Department of Computer Science Technical Report TR 94-1455 (.pdf), September 1994. With D. Gries.

Verifying Programs that use Causally-ordered Message-passing. Science of Computer Programming 24, 2 (1995), 105--128. Earlier version available as Cornell University Department of Computer Science Technical Report TR 94-1423 (scanned .pdf), May 1994. With S. Stoller.

Hypervisor-based Fault-Tolerance. ACM Transactions on Computer Systems 14, 1 (February 1996), 80--107. Earlier version available as Cornell University Department of Computer Science Technical Report TR 95-1495 (.pdf), March 1995. With T. Bressoud.

Adding the everywhere operator to propositional logic. Journal of Logic and Computation 8, 1 (February 1998), 119--129. Earlier version available as Cornell University Department of Computer Science Technical Report TR 96-1583 (.pdf), May 1996. With D. Gries.

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. Earlier version available as Cornell University Department of Computer Science Technical Report TR 99-1759 (.pdf), July 1999.

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.  Earlier version available as Cornell University Department of Computer Science Technical Report TR 2000-1828, December 7, 2000. With Lidong Zhou and Robbert van Renesse.

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 systemIEEE 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 system. (scanned .pdf) Formal Methods in System Design, Volume 26, Number 2 (March 2005), 183--196.  With Scott Stoller. Earlier version is available here (scanned .pdf).

APSS: Proactive secret sharing in asynchronous systemsACM Transactions on Information and System Security 8, 3 (August 2005), 259--286.  Earlier version available as Cornell University Department of Computer Science Technical Report TR 2002-1877 (scanned .pdf), October 2002. With Lidong Zhou and Robbert van Renesse.

Implementing trustworthy services using replicated state machinesIEEE Security and Privacy, Volume 3, Number 5 (September/October 2005), 34--43. Earlier version available as Cornell University Department of Computer Science 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 University Department of Computer Science Technical Report TR 2003-1908, August 2003. With Kevin W. Hamlen and Greg Morrisett.

The monoculture risk put into contextIEEE Security and Privacy 7, 1 (January/February 2009), 14--17. With Ken Birman.

Quantifying Information Flow with Beliefs.  Invited paper.  Journal of Computer Security 17(5), 655--701, 2009.  Preliminary version available as Cornell Computing and Information Science Technical Report, February 2005. With Michael R. Clarkson and Andrew C. Myers.

Proactive ObfuscationACM Transactions on Computer Systems 28, 2 (July 2010), 1--54. Preliminary version available as Cornell Computing and Information Science Technical Report, March 28, 2009. With Tom Roeder.

Independence from obfuscation: A semantic framework for diversity. Journal of Computer Security 18, 5 (August 2010), 701--749.  (Extended version of a paper with the same title appearing in  Proceedings 19th IEEE Computer Security Foundations Workshop.)  With Riccardo Pucella.

Hyperproperties.  Journal of Computer Security 18. 6 (September 2010), 1157--1210.  Available as Cornell Computing and Information Science Technical Report, December 22, 2008.  With Michael R. Clarkson.

Nexus Authorization Logic (NAL): Design Rationale and Applications. ACM Transactions on Information and System Security 14, 1 (May 2011). Earlier version available as Cornell Computing and Information Science Technical Report, September 14, 2009. With Kevin Walsh and Emin Gun Sirer .

Multi-Verifier SignaturesJournal of Cryptography 25, 2 (April 2012), 310--348.  Also available as Cornell Computing and Information Science Technical Report, August 15, 2009. With Tom Roeder and Rafael Pass.

Federated identity management systems:  A privacy-based characterization. IEEE Security & Privacy 11, 5 (September/October 2013), 36--48.  Preliminary version available as Cornell Computing and Information Science Technical Report. October 2012.  With Eleanor Birrell.


 

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. Earlier version available as Cornell University Department of Computer Science Technical Report TR 79-374 (scanned .pdf), March 1979. With A. J. Bernstein.

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. Earlier version available as Cornell University Department of Computer Science Technical Report TR 79-392 (scanned .pdf), September 1979.

The master key problem. Proc. 1980 Symposium on Security and Privacy (Oakland, California, April 1980), IEEE Computer Society, Oakland, California, 103--107. Earlier version available as Cornell University Department of Computer Science Technical Report TR 80-409 (scanned .pdf). With D. Denning.

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.

Constraints: 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. Earlier version available as Cornell University Department of Computer Science Technical Report TR 84-635 (scanned .pdf), September 1984. With L. Lamport.

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. Earlier version available as Cornell University Department of Computer Science Technical Report TR 85-677 (scanned .pdf). With R. E. Johnson.

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. (.pdf) (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. (scanned .pdf) 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. Earlier version available as Cornell University Department of Computer Science Technical Report TR 92-1265 (scanned .pdf), January 1992. With Budhiraja,N., Marzullo, K., and Toueg, S.

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. Also available as Cornell University Department of Computer Science Technical Report TR 94-1409 (.pdf), October 1994.With L. Fix.

Hybrid verification by exploiting the environmentFormal 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. (.pdf) 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 approachesProc. 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 TACOMAProc. 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 systemsProc. 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 agentryProc. 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. (.pdf) 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. (.pdf) 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. (.pdf) 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 inspectionProceedings 2000 IEEE Symposium on Security and Privacy (Oakland, California, May 2000), IEEE Computer Society, Los Alamitos, California, 246--255. Also available as Cornell University Department of Computer Science Technical Report TR 2000-1786 (.pdf), February 2000. With Ulfar Erlingsson.

Open source in security: Visiting the bizarreProceedings 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 (.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 servicePeer-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 (.pdf), February 2004.  With William Josephson and Emin Gun Sirer.

Distributed blinding for distributed ElGamal re-encryptionProceedings 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 (.pdf), January 2004.  With Lidong Zhou, Michael A. Marsh, and Anna Redz.

Belief in information flowProceedings 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 .NETProceedings 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 Department of Computer Science 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 Department of Computer Science 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 TR 1813/9480. January 2008.  With Michael R. Clarkson.

Device driver safety through a reference validation mechanism. Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation OSDI '08, (San Diego, CA, December 2008),  241--254. With Dan Williams, Patrick Reynolds, Kevin Walsh, and Emin Gun Sirer.

Quantification of IntegrityProceedings 23rd IEEE Computer Security Foundations Symposium (Edinburgh, UK, July 2010), 28--43.  Also available as Computing and Information Sciences Technical Report.  February 12, 2010.  With Michael Clarkson.

NetQuery:  A Knowledge Plane for Reasoning about Network PropertiesProceedings of ACM SIGCOMM 2011 (Toronto, Ontario, Canada August 2011), 278--289.  With Alan Shieh and Emin Gun Sirer.


Logical Attestation: An Authorization Architecture for Trustworthy Computing. SOSP'11 Proceedings of 23rd ACM Symposium on Operating Systems Principles (Cascais, Portugal, October 2011), 249--264.  Also available as Cornell Computing and Information Science Technical Report. With Emin Gun Sirer, Willen De Bruijin, Patrick Reynolds, Alan Shieh, Kevin Walsh, and Dan Williams. (Click here for 1-column version.)

When not all bits are equal:  Incorporating "worth" into information-flow measures.  Principles of Security and Trust POST 2014 (Grenoble, France, April 2014) Lecture Notes in Computer Science, vol 8414.  M. Abadi and S. Kremer Eds. 120—139.  Preliminary version available as Cornell Computing and Information Science Technical Report, April 2013.  With Mario Alvim and Andre Scedrov.


 

Other Publications

Scheduling in Concurrent Pascal. Operating Systems Review 12, 2 (April 1978), 15--21. With A. J. Bernstein. Cornell University Department of Computer Science Technical Report TR 79-365 (.pdf).

Synchronization and concurrent programming. Handbook of Electrical and Computer Engineering, John Wiley and Sons, 1983. Cornell University Department of Computer Science Technical Report TR 80-425 (.pdf).

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 . Cornell University Department of Computer Science Technical Report TR 80-440 (.pdf).


Book review: The Practical Guide to Structured Systems Design. IEEE Spectrum 18, 3 (March 1981), 92.

The fail-stop processor approach. (.pdf) Invited chapter in Reliability in Distributed Software and Database Systems (B. Bhargava, ed.), Von Nostrand Reinhold Comany, New York 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''. (.pdf) Software Engineering Notes 13, 3 (July 1988), 18--19. With L. Lamport.

Critical (of) issues in real-time systems: A position paper. (scanned .pdf) (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. Cornell University Department of Computer Science Technical Report TR 89-1037 (scanned .pdf).

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 . Cornell University Department of Computer Science Technical Report TR 91-1217 (scanned .pdf).

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. Cornell University Department of Computer Science Technical Report TR 91-1238 (scanned .pdf).

Reasoning about real-time actions.Proc. of Fourth Annual Workshop, Foundations of Real-time Computing Initiative, (Washington, D.C., October 1991), Office of Naval Research, 85--91. And Bard Bloom and Keith Marzullo.


Lower bounds for primary-backup implementations of BOFO services. (.pdf) 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? (.pdf) Chapter 2, Distributed Systems, 2nd Edition (S. Mullender, ed.), Addison Wesley, 1993, 17--25.

Replication management using the state machine approach. (.pdf) Chapter 7,
Distributed Systems, 2nd Edition (S. Mullender, ed.), Addison Wesley, 1993, 169--195.

The primary-backup approach. (.pdf) 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. (.pdf) 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. (.pdf) Foundations of Dependable Computing, Paradigms for Dependable Applications, Kluwer Academic Publishers, 1994, 39--54. With K. Marzullo and J. Dehn. Cornell University Department of Computer Science Technical Report TR 94-1417 (scanned .pdf).

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 underspecificationComputer 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. (.pdf) 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.

What Tacoma Taught Us. (.pdf) 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
. (.pdf) 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. Cornell University Department of Computer Science Technical Report TR 98-1686 (.pdf).


International review of UK research in Computer Science. EPSRC, BCS, IEE.  November 2001.  Fred B. Schneider and Mike Rodd, editors.

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.


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.

Language-Based Security for Malicious Mobile CodeDepartment 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.

Interview:  Silver Bullet Talks with Fred Schneider.  Interview by Gary McGraw. IEEE Security and Privacy Magazine 7, 6 (November/December 2009), 5--7.

Beyond traces and independenceDependable and Historic Computing.  Essays Dedicated to Brian Randell on the Occasion of His 75th Birthday, Lecture Notes in Computer Science, Vol. 6875 (Cliff Jones and John Lloyd, eds).  Springer Verlag, 2011, 479--485.

Computing Researchers Get 'Schooled' on Science Policy at CCC WorkshopComputing Research News.  Volume 24, No. 1 (January 2012).  With Peter Harsha.

Computing Researchers Get 'Schooled' on Science Policy at LiSPI 2013. Computing Research News. Volume 25, No. 7 (August 2013). With Peter Harsha.

Editorials

Communications of the ACM

On Concurrent Programming. Invited "Inside Risks" column. Communications of the ACM 41, 4 (April 1998), 128.

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.

Secure Systems Conundrum. Invited "Inside Risks'' column. Communications of the ACM 45, 10 (October 2002), 160. 

Program Committee Overload in Systems
. Communications of the ACM 52, 05 (May 2009),34--37. With Ken Birman.

IEEE Security and Privacy Magazine

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. 

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.

Technology Scapegoats and Policy Saviors. Editorial. IEEE Security & Privacy 5, 5 (September/October 2007), 3--4.

Network Neutrality versus Internet Trustworthiness. Editorial. IEEE Security & Privacy 6, 4 (July/August 2008), 3--4.

Accountability for Perfection. Editorial. IEEE Security & Privacy 7, 2 (March/April 2009), 3--4.

Labeling-in Security.  Editorial. IEEE Security & Privacy 7, 6 (November/December 2009), 3.

Fumbling the Future, Again.  Editorial.  IEEE Security & Privacy 8, 4 (July/August 2010), 3

A Doctrinal Thesis.  Editorial.  IEEE Security & Privacy 9, 4 (July/August 2011), 3--4.  With Deirdre Mulligan.

Breaking-in Research.  Editorial.  IEEE Security & Privacy 11, 2 (March/April 2013), 3-4.

Cybersecurity Education in Universities.  Editorial.  IEEE Security & Privacy 11, 4 (July/August 2013), 3-4.

Unpublished Tech Reports

Medium Term Scheduling and Equivalence of Synchronous and Asynchronous Operation. State University of New York at Stony Brook Department of Computer Science Technical Report #72 (scanned .pdf), June 1977. With E.A. Akkoyunlu and A.J. Bernstein.

Use of a Formalism for Modeling the Protection Aspects of Operating Systems.
State University of New York at Stony Brook Department of Computer Science Technical Report #74 (scanned .pdf), July 1977. With E.A. Akkoyunlu.

Mechanisms for Specifying Scheduling Policies. (.pdf) Cornell University Department of Computer Science Technical Report TR 79-365 (scanned .pdf), January 1979.  With A. J. Bernstein.

On Restrictions to Ensure Reproducible Behavior in Concurrent Programs. Cornell University Department of Computer Science Technical Report TR 79-374 (scanned .pdf), 1979.  With A. J. Bernstein.

Personal Keys, Group Keys and Master Keys. Cornell University Department of Computer Science Technical Report TR 80-409 (scanned .pdf), 1980.  With Dorothy E. Denning.

Three Surveys on Operating System Topics
. Cornell University Department of Computer Science Technical Report TR 80-425 (scanned .pdf), May 1980.  With Gregory R. Andrews.

Detecting Distributed Termination When Processors can Fail. Cornell University Department of Computer Science Technical Report TR 80-449 (scanned .pdf), December 1980.  With G. W. Lerman.

Cornell Local Network (CLONE) Interface Unit Principles of Operation. Cornell University Department of Computer Science Technical Report TR 81-461 (scanned .pdf), May 1981.

An Approach to Designing Fault-Tolerant Computing Systems. Cornell University Department of Computer Science Technical Report TR 81-479 (scanned .pdf), November 1981.  With Richard Schlichting.

A Distributed Path Algorithm and its Correctness Proof. Cornell University Department of Computer Science Technical Report TR 83-556 (scanned .pdf), June 1983.  With David D. Wright.

Documentation for the CHIP Computer System. Cornell University Department of Computer Science Technical Report TR 83-584 (scanned .pdf), December 1983.  With Ozalp Babaoglu, Mimi Bussan , Rogerio Drummond.

Constraints:  A Uniform Approach to Aliasing and Typing. Cornell University Department of Computer Science Technical Report TR 84-635 (scanned .pdf), September 1984.  With Leslie Lamport.

The HOCA Operating System Specifications. Cornell University Department of Computer Science Technical Report TR 83-585 (scanned .pdf), December 1983.  With Ozalp Babaoglu.

Understanding Protocols for Byzantine Clock Synchronization
. Cornell University Department of Computer Science Technical Report TR 87-859 (scanned .pdf), August 1987.

Decomposing Properties into Safety and Liveness using Predicate Logic. Cornell University Department of Computer Science Technical Report TR 87-874 (scanned .pdf), October 1987.

Pretending Atomicity. (.pdf) Digital Equipment Corporation Systems Research Center Research Report 44, May 1989.

Verifying Safety Properties Using Non-deterministic Infinite-star Automata. Cornell University Department of Computer Science Technical Report TR 89-1036 (scanned .pdf), September 1989.  With Nils Klarlund.

An Assertional Characterization of Serializability. Cornell University Department of Computer Science Technical Report  TR 89-1039 (scanned .pdf), September 1989.  With E. Robert McCurley.

Priority Inversion and Its Prevention. Cornell University Department of Computer Science Technical Report TR 90-1088 (scanned .pdf), February 1990.  With Ozalp Babaoglu, Keith Marzullo.

Progress Measures for Verification Involving Non- determinism
. Cornell University Department of Computer Science Technical Report TR 90-1167 (scanned .pdf), November 1990.  With Nils Klarlund.

The Trainset Railroad Simulation. Cornell University Department of Computer Science Technical Report TR 93-1329 (.pdf), February 1993.  With Richard Brown, Jacob Aizikowitz, Thomas C. Bressoud, Tony Lekas.

Putting Time Into Proof Outlines
. Cornell University Department of Computer Science Technical Report TR 93-1333 (scanned .pdf), March 1993.  With Bard Bloom, Keith Marzullo.

A Graphical Interface for CHIP. Cornell University Department of Computer Science Technical Report TR 96-1591 (.pdf), June 1996, With Lorenzo Alvisi.


Critical Infrastructures You Can Trust:  Where Telecommunications Fits. Cornell University Department of Computer Science Technical Report TR 98-1717 (.pdf), October 1998.  With Steven Bellovin, Alan Inouye.

Using external security monitors to secure BGP.  With Patrick Reynolds, Oliver Kennedy, and Emin Gun Sirer.

Design Principles for Isolation KernelsUniversity of Tromso, MUNIN Technical Report 2011-70, October 2011.  With Age Kvalnes, Dag Johansen, Robbert van Renesse, and Steffen Viken Valvag


Costs of security in the PFS file system.   Cornell Computing and Information Science Technical Report, July 25, 2012. With Kevin Walsh.