Selected Papers by Geoffrey Smith

This group of papers considers the secure information flow problem: if each variable in a program is classified as either high or low security, how can we ensure that information in the high variables is not leaked to the low variables? The papers describe static analyses, in the form of type systems, that are sufficient to guarantee secure information flow.

• Adversaries and Information Leaks, Geoffrey Smith, in Gilles Barthe and Cédric Fournet, editors, TGC 2007 (Trustworthy Global Computing), volume 4912 of Lecture Notes in Computer Science, pp. 383-400. Springer-Verlag, 2008.
• Fast Probabilistic Simulation, Nontermination, and Secure Information Flow, Geoffrey Smith and Rafael Alpízar, Proc. ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, pp. 67-71, San Diego, California, June 2007.
• Secure Information Flow with Random Assignment and Encryption, Geoffrey Smith and Rafael Alpízar, Proc. 4th ACM Workshop on Formal Methods in Security Engineering, pp. 33-43, Alexandria, Virginia, November 2006.
• Improved Typings for Probabilistic Noninterference in a Multi-Threaded Language, Geoffrey Smith, Journal of Computer Security 14(6), pp. 591-623, December 2006.
• Principles of Secure Information Flow Analysis, Geoffrey Smith, Chapter 13 (pp. 291-307) of Malware Detection, edited by Mihai Christodorescu, Somesh Jha, Douglas Maughan, Dawn Song, and Cliff Wang, Springer-Verlag, 2007.
• Type Inference and Informative Error Reporting for Secure Information Flow, Zhenyue Deng and Geoffrey Smith, Proc. ACMSE 2006: 44th ACM Southeast Conference, pp. 543-548, Melbourne, Florida, March 2006.
• Lenient Array Operations for Practical Secure Information Flow, Zhenyue Deng and Geoffrey Smith, Proc. 17th IEEE Computer Security Foundations Workshop, pp. 115-124, Pacific Grove, California, June 2004.
• Secure Information Flow Analysis: A Science of Hacking?, Geoffrey Smith, slides for a seminar given at FIU in October 2003.
• Probabilistic Noninterference through Weak Probabilistic Bisimulation, Geoffrey Smith, Proc. 16th IEEE Computer Security Foundations Workshop, pp. 3-13, Pacific Grove, California, June 2003.
• A New Type System for Secure Information Flow, Geoffrey Smith, Proc. 14th IEEE Computer Security Foundations Workshop, pp. 115-125, Cape Breton, Nova Scotia, June 2001.
• Verifying Secrets and Relative Secrecy, Dennis Volpano and Geoffrey Smith, Proc. 27th ACM Symposium on Principles of Programming Languages, pp. 268-276, Boston Massachusetts, January 2000.
• Probabilistic Noninterference in a Concurrent Language, Dennis Volpano and Geoffrey Smith, Journal of Computer Security 7(2,3), pp. 231-253, November 1999.
• Confinement Properties for Multi-Threaded Programs, Geoffrey Smith and Dennis Volpano, Electronic Notes in Theoretical Computer Science 20, 1999.
• Language Issues in Mobile Program Security, Dennis Volpano and Geoffrey Smith, in Mobile Agents and Security, G. Vigna (Ed.), volume 1419 of Lecture Notes in Computer Science, pp. 25-43. Springer Verlag, 1998.
• Secure Information Flow in a Multi-threaded Imperative Language, Geoffrey Smith and Dennis Volpano, Proc. 25th ACM Symposium on Principles of Programming Languages, pp. 355-364, San Diego, California, January 1998.
• Eliminating Covert Flows with Minimum Typings, Dennis Volpano and Geoffrey Smith, Proc. 10th IEEE Computer Security Foundations Workshop, pp. 156-168, Rockport, Massachusetts, June 1997.
• A Type-Based Approach to Program Security, Dennis Volpano and Geoffrey Smith, Proc. TAPSOFT'97, LNCS 1214, pp. 607-621, Lille, France, April 1997.
• A Sound Type System for Secure Flow Analysis, Dennis Volpano, Geoffrey Smith and Cynthia Irvine, Journal of Computer Security 4(3), pp. 167-187, December 1996.

Here is some work on intrusion detection:

• Anatomy of a Real-time Intrusion Prevention System, Ricardo Koller, Raju Rangaswami, Joseph Marrero, Igor Hernandez, Geoffrey Smith, Mandy Barsilai, Silviu Necula, S. Masoud Sadjadi, Tao Li, and Krista Merrill, Proc. 5th IEEE International Conference on Autonomic Computing, pp. 151-160, Chicago, Illinois, June 2008.

Here is some work on minimal nondeterministic finite automata:

• Inductive Bases and their Application to Searches for Minimal Unary NFAs, Geoffrey Smith, Proc. ACMSE 2006: 44th ACM Southeast Conference, pp. 470-475, Melbourne, Florida, March 2006.

The following paper considers the use of XML for managing role-based access control policies:

• Managing Security Policies in a Distributed Environment Using eXtensible Markup Language (XML), Nathan Vuong, Geoffrey Smith, and Yi Deng, Proc. 16th ACM Symposium on Applied Computing, pp. 405-411, Las Vegas, NV, March 2001.

The following papers present sound polymorphic type systems for imperative languages. By considering traditional variables rather than Standard ML's references, we are able to type programs less restrictively.

• A Sound Polymorphic Type System for a Dialect of C, Geoffrey Smith and Dennis Volpano, Science of Computer Programming 32(2-3), pp. 49-72, 1998.
• Polymorphic Typing of Variables and References, Geoffrey Smith and Dennis Volpano, ACM Transactions on Programming Languages and Systems 18(3), pp. 254-267, May 1996.
• A Type Soundness Proof for Variables in LCF ML, Dennis Volpano and Geoffrey Smith, Information Processing Letters 56(3), pp. 141-146, November 1995.

The following papers, based on my PhD dissertation work, address the problem of extending Hindley/Milner type inference to allow overloaded operators and atomic subtyping.

• Principal Type Schemes for Functional Programs with Overloading and Subtyping, Geoffrey S. Smith, Science of Computer Programming 23(2-3), pp. 197-226, December 1994.
• On the Complexity of ML Typability with Overloading, Dennis M. Volpano and Geoffrey S. Smith, Proc. 5th Conference on Functional Programming Languages and Computer Architecture, LNCS 523, pp. 15-28, Cambridge, Massachusetts, August 1991.
• Polymorphic Type Inference for Languages with Overloading and Subtyping, Geoffrey Seward Smith, Cornell University Ph.D. dissertation, August 1991. (A reconstructed version.)

The materials on this page are based upon work supported by the National Science Foundation under Grant Nos. HRD-0317692, CCR-990951, CCR-9612176, and CCR-9596113.

Geoffrey Smith's homepage