The SLam calculus

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback
Take a look at the new version of this page: [ beta version ]. Tell us what you think.

The SLam calculus: programming with secrecy and integrity

Full text

Pdf (1.78 MB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents

San Diego, California, United States

Pages: 365 - 377

Year of Publication: 1998

ISBN:0-89791-979-3

Authors

Nevin Heintze	Bell Laboratories, Lucent Technologies, 700 Mountain Avenue, Murray Hill, NJ
Jon G. Riecke	Bell Laboratories, Lucent Technologies, 700 Mountain Avenue, Murray Hill, NJ

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 7, Downloads (12 Months): 52, Citation Count: 78

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/268946.268976 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Martín Abadi, Secrecy by Typing inSecurity Protocols, Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software, p.611-638, September 23-26, 1997
	2	Martín Abadi , Andrew D. Gordon, A calculus for cryptographic protocols: the spi calculus, Proceedings of the 4th ACM conference on Computer and communications security, p.36-47, April 01-04, 1997, Zurich, Switzerland [doi>10.1145/266420.266432]
	3	Gregory R. Andrews , Richard P. Reitman, An Axiomatic Approach to Information Flow in Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.56-76, Jan. 1980 [doi>10.1145/357084.357088]
	4	Jean-Pierre Banâtre , Ciarán Bryce , Daniel Le Métayer, Compile-Time Detection of Information Flow in Sequential Programs, Proceedings of the Third European Symposium on Research in Computer Security, p.55-73, November 07-09, 1994
	5	L Cardelli, Amber, Proc. of the thirteenth spring school of the LITP on Combinators and functional programming languages, p.21-47, October 1986, Val d'Ajol, France
	6	Dorothy Elizabeth Robling Denning, Secure information flow in computer systems., 1975
	7	Dorothy E. Denning, A lattice model of secure information flow, Communications of the ACM, v.19 n.5, p.236-243, May 1976 [doi>10.1145/360051.360056]
	8	Dorothy E. Denning , Peter J. Denning, Certification of programs for secure information flow, Communications of the ACM, v.20 n.7, p.504-513, July 1977 [doi>10.1145/359636.359712]
	9	M. Felleisen, The theory and practice of first-class prompts, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.180-190, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73576]
	10	D. McCullough. Noninterference and the composabillty of security properties. In 19881EEE Symposium on SecuriJy and Privacy, pages 177-186, 1988.
	11	Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
	12	John C. Mitchell, Foundations of programming languages, MIT Press, Cambridge, MA, 1996
	13	Andrew C. Myers , Barbara Liskov, A decentralized model for information flow control, Proceedings of the sixteenth ACM symposium on Operating systems principles, p.129-142, October 05-08, 1997, Saint Malo, France
	14	J. Palsberg and P. ~rba~k. Trust in the X-calculus. In Proceedings of the 1995 Static Analysis Symposium, number 983 hL Leer. Notes in Computer $ci. Spdnger-Verlag, 1995.
	15	A. M. Pitts. Relational properties of domains. Information and Computation, t27:66-90, 1996.
	16	G. D. Plotkin. A structural appr6aeh to operational semantics. Technical Report DAIMI FN-19, Aarhus Univ., Com. puti~r Science Dept., Denmark, 1981.
	17	G. D. Plotkin. (Towards a) logic for computable functions, Unpublished manuscript, CSLI Summer School Notes, 1985,
	18	J. C. Reynolds. Types, abstraction and parametric polyrnorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513-523. Noah Holland, Amsterdam, 1983.
	19	Geoffrey Smith , Dennis Volpano, Secure information flow in a multi-threaded imperative language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.355-364, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268975]
	20	J.-P. Talpin and P. Jouvelot. Polymorphie type, region and effect inference. Journal of Functional Programming, 2:245- 271, 1992.
	21	Dennis Volpano , Geoffrey Smith, Eliminating Covert Flows with Minimum Typings, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.156, June 10-12, 1997
	22	Dennis M. Volpano , Geoffrey Smith, A Type-Based Approach to Program Security, Proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.607-621, April 14-18, 1997
	23	Dennis Volpano , Cynthia Irvine , Geoffrey Smith, A sound type system for secure flow analysis, Journal of Computer Security, v.4 n.2-3, p.167-187, Jan. 1996

CITED BY 78

	Nobuko Yoshida , Matthew Hennessy, Assigning types to processes, Information and Computation, v.174 n.2, p.143-179, May 1 2002
	Nael B. Abu-Ghazaleh , Dhananjay S. Phatak, Verification caching: towards efficient and secure mobile code execution environments, Proceedings of the 2002 ACM symposium on Applied computing, March 11-14, 2002, Madrid, Spain
	Steve Zdancewic , Lantian Zheng , Nathaniel Nystrom , Andrew C. Myers, Untrusted hosts and confidentiality: secure program partitioning, ACM SIGOPS Operating Systems Review, v.35 n.5, Dec. 2001
	Jan Vitek , Boris Bokowski, Confined types, ACM SIGPLAN Notices, v.34 n.10, p.82-96, Oct. 1999
	Christopher League , Zhong Shao , Valery Trifonov, Representing Java classes in a typed intermediate language, ACM SIGPLAN Notices, v.34 n.9, p.183-196, Sept. 1999
	Matthew Hennessy , James Riely, Resource access control in systems of mobile agents, Information and Computation, v.173 n.1, p.82-120, February 25, 2002
	Andrew C. Myers , Barbara Liskov, Protecting privacy using the decentralized label model, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.4, p.410-442, Oct. 2000
	Naoya Nitta , Hiroyuki Seki , Yashiaki Takata, Security verification of programs with stack inspection, Proceedings of the sixth ACM symposium on Access control models and technologies, p.31-40, May 2001, Chantilly, Virginia, United States
	Steve Zdancewic , Dan Grossman , Greg Morrisett, Principals in programming languages: a syntactic proof technique, ACM SIGPLAN Notices, v.34 n.9, p.197-207, Sept. 1999
	Martín Abadi, Secrecy by typing in security protocols, Journal of the ACM (JACM), v.46 n.5, p.749-786, Sept. 1999
	Kohei Honda , Nobuko Yoshida, A uniform type structure for secure information flow, ACM SIGPLAN Notices, v.37 n.1, p.81-92, Jan. 2002
	Matthew Hennessy , James Riely, Information flow vs. resource access in the asynchronous pi-calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.5, p.566-591, September 2002
	James Riely , Matthew Hennessy, Trust and partial typing in open systems of mobile agents, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.93-104, January 20-22, 1999, San Antonio, Texas, United States
	Thomas Colcombet , Pascal Fradet, Enforcing trace properties by program transformation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-66, January 19-21, 2000, Boston, MA, USA
	Geoffrey Smith , Dennis Volpano, Secure information flow in a multi-threaded imperative language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.355-364, January 19-21, 1998, San Diego, California, United States
	Naoya Nitta , Yoshiaki Takata , Hiroyuki Seki, An efficient security verification method for programs with stack inspection, Proceedings of the 8th ACM conference on Computer and Communications Security, November 05-08, 2001, Philadelphia, PA, USA
	Martín Abadi , Bruno Blanchet, Analyzing security protocols with secrecy types and logic programs, ACM SIGPLAN Notices, v.37 n.1, p.33-44, Jan. 2002
	François Pottier , Vincent Simonet, Information flow inference for ML, ACM SIGPLAN Notices, v.37 n.1, p.319-330, Jan. 2002
	Steve Zdancewic , Lantian Zheng , Nathaniel Nystrom , Andrew C. Myers, Secure program partitioning, ACM Transactions on Computer Systems (TOCS), v.20 n.3, p.283-328, August 2002
	François Pottier , Sylvain Conchon, Information flow inference for free, ACM SIGPLAN Notices, v.35 n.9, p.46-57, Sept. 2000
	Martín Abadi , Anindya Banerjee , Nevin Heintze , Jon G. Riecke, A core calculus of dependency, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.147-160, January 20-22, 1999, San Antonio, Texas, United States
	Christian Skalka , Scott Smith, Static enforcement of security with types, ACM SIGPLAN Notices, v.35 n.9, p.34-45, Sept. 2000
	Dan Grossman , Greg Morrisett , Steve Zdancewic, Syntactic type abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.6, p.1037-1080, Nov. 2000
	R. Barbuti , C. Bernardeschi , N. De Francesco, Abstract interpretation of operational semantics for secure information flow, Information Processing Letters, v.83 n.2, p.101-108, 31 July 2002
	Gleb Naumovich, A conservative algorithm for computing the flow of permissions in Java programs, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
	C. Bodei , P. Degano , F. Nielson , H. Riis Nielson, Flow logic for Dolev-Yao secrecy in cryptographic processes, Future Generation Computer Systems, v.18 n.6, p.747-756, May 2002
	Peter Sewell , Jan Vitek, Secure composition of untrusted code: box π, wrappers, and causality types, Journal of Computer Security, v.11 n.2, p.135-187, May 2003
	John Hale , Mauricio Papa , Sujeet Shenoi, Programmable access control, Journal of Computer Security, v.11 n.3, p.331-351, 1 March 2003
	Heiko Mantel , Andrei Sabelfeld, A unifying approach to the security of distributed and multi-threaded programs, Journal of Computer Security, v.11 n.4, p.615-676, 01/01/2004
	Eijiro Sumii , Benjamin C. Pierce, Logical relation for encryption, Journal of Computer Security, v.11 n.4, p.521-554, 01/01/2004
	Nobuko Yoshida, Channel dependent types for higher-order mobile processes, ACM SIGPLAN Notices, v.39 n.1, p.147-160, January 2004
	Stephen Tse , Steve Zdancewic, Translating dependency into parametricity, ACM SIGPLAN Notices, v.39 n.9, September 2004
	Andrew C. Myers, JFlow: practical mostly-static information flow control, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.228-241, January 20-22, 1999, San Antonio, Texas, United States
	Johan Agat, Transforming out timing leaks, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.40-53, January 19-21, 2000, Boston, MA, USA
	Xavier Leroy, Java Bytecode Verification: Algorithms and Formalizations, Journal of Automated Reasoning, v.30 n.3-4, p.235-269, 2003
	François Pottier , Vincent Simonet, Information flow inference for ML, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.1, p.117-158, January 2003
	Stephen Chong , Andrew C. Myers, Security policies for downgrading, Proceedings of the 11th ACM conference on Computer and communications security, October 25-29, 2004, Washington DC, USA
	Eijiro Sumii , Benjamin C. Pierce, A bisimulation for type abstraction and recursion, ACM SIGPLAN Notices, v.40 n.1, p.63-74, January 2005
	Martín Abadi , Bruno Blanchet, Analyzing security protocols with secrecy types and logic programs, Journal of the ACM (JACM), v.52 n.1, p.102-146, January 2005
	Roberto Barbuti , Cinzia Bernardeschi , Nicoletta De Francesco, Checking security of Java bytecode by abstract interpretation, Proceedings of the 2002 ACM symposium on Applied computing, March 11-14, 2002, Madrid, Spain
	Nicoletta De Francesco , Antonella Santone , Luca Tesei, Abstract interpretation and model checking for checking secure information flow in concurrent systems, Fundamenta Informaticae, v.54 n.2-3, p.195-211, February 2003
	Martín Abadi , Bruno Blanchet, Secrecy types for asymmetric communication, Theoretical Computer Science, v.298 n.3, p.387-415, 11 April 2003
	Sebastian Hunt , David Sands, On flow-sensitive security types, ACM SIGPLAN Notices, v.41 n.1, p.79-90, January 2006
	Mads Dam, Decidability and proof systems for language-based noninterference relations, ACM SIGPLAN Notices, v.41 n.1, p.67-78, January 2006
	Andrew C. Myers , Andrei Sabelfeld , Steve Zdancewic, Enforcing robust declassification and qualified robustness, Journal of Computer Security, v.14 n.2, p.157-196, January 2006
	Scott F. Smith , Mark Thober, Refactoring programs to secure information flows, Proceedings of the 2006 workshop on Programming languages and analysis for security, June 10-10, 2006, Ottawa, Ontario, Canada
	C. Bernardeschi , N. De Francesco , G. Lettieri , L. Martini, Checking secure information flow in java bytecode by code transformation and standard bytecode verification, Software—Practice & Experience, v.34 n.13, p.1225-1255, 10 November 2004
	Chuchang Liu , Mehmet A. Orgun, Towards security labelling, Proceedings of the 29th Australasian Computer Science Conference, p.69-76, January 16-19, 2006, Hobart, Australia
	Andrew D. Gordon , Alan Jeffrey, Types and effects for asymmetric cryptographic protocols, Journal of Computer Security, v.12 n.3,4, p.435-483, May 2004
	Neil Vachharajani , Matthew J. Bridges , Jonathan Chang , Ram Rangan , Guilherme Ottoni , Jason A. Blome , George A. Reis , Manish Vachharajani , David I. August, RIFLE: An Architectural Framework for User-Centric Information-Flow Security, Proceedings of the 37th annual IEEE/ACM International Symposium on Microarchitecture, p.243-254, December 04-08, 2004, Portland, Oregon
	Kao-Shing Hwang , Yu-Jen Chen , Hai-Chun Hong, Autonomous Exploring System Based on Ultrasonic Sensory Information, Journal of Intelligent and Robotic Systems, v.39 n.3, p.307-331, March 2004
	Hiroshi Unno , Naoki Kobayashi , Akinori Yonezawa, Combining type-based analysis and model checking for finding counterexamples against non-interference, Proceedings of the 2006 workshop on Programming languages and analysis for security, June 10-10, 2006, Ottawa, Ontario, Canada
	Gilles Barthe , Tamara Rezk , Amitabh Basu, Security types preserving compilation, Computer Languages, Systems and Structures, v.33 n.2, p.35-59, July, 2007
	Torben Amtoft , Anindya Banerjee, A logic for information flow analysis with an application to forward slicing of simple imperative programs, Science of Computer Programming, v.64 n.1, p.3-28, January, 2007
	Scott F. Smith , Mark Thober, Improving usability of information flow security in java, Proceedings of the 2007 workshop on Programming languages and analysis for security, June 14-14, 2007, San Diego, California, USA
	Nicoletta De Francesco , Luca Martini, Instruction-level security analysis for information flow in stack-based assembly languages, Information and Computation, v.205 n.9, p.1334-1370, September, 2007
	Eijiro Sumii , Benjamin C. Pierce, A bisimulation for type abstraction and recursion, Journal of the ACM (JACM), v.54 n.5, p.26-es, October 2007
	Janus Dam Nielsen , Michael I. Schwartzbach, A domain-specific programming language for secure multiparty computation, Proceedings of the 2007 workshop on Programming languages and analysis for security, June 14-14, 2007, San Diego, California, USA
	Chuchang Liu , Angela Billard , Maris Ozols , Nikifor Jeremic, Access control models and security labelling, Proceedings of the thirtieth Australasian conference on Computer science, p.181-190, January 30-February 02, 2007, Ballarat, Victoria, Australia
	Stephen Tse , Steve Zdancewic, Run-time principals in information-flow type systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.1, p.6-es, November 2007
	Cinzia Bernardeschi , Nicoletta De Francesco , Giuseppe Lettieri, Concrete and Abstract Semantics to Check Secure Information Flow in Concurrent Programs, Fundamenta Informaticae, v.60 n.1-4, p.81-98, January 2004
	Feng Qin , Cheng Wang , Zhenmin Li , Ho-seop Kim , Yuanyuan Zhou , Youfeng Wu, LIFT: A Low-Overhead Practical Information Flow Tracking System for Detecting Security Attacks, Proceedings of the 39th Annual IEEE/ACM International Symposium on Microarchitecture, p.135-148, December 09-13, 2006
	Anindya Banerjee , David A. Naumann, Stack-based access control and secure information flow, Journal of Functional Programming, v.15 n.2, p.131-177, March 2005
	Karl Crary , Aleksey Kliger , Frank Pfenning, A monadic analysis of information flow security with mutable state, Journal of Functional Programming, v.15 n.2, p.249-291, March 2005
	Kohei Honda , Nobuko Yoshida, Noninterference through flow analysis, Journal of Functional Programming, v.15 n.2, p.293-349, March 2005
	Steve Zdancewic , Andrew C. Myers, Secure Information Flow via Linear Continuations, Higher-Order and Symbolic Computation, v.15 n.2-3, p.209-234, September 2002
	Andrei Sabelfeld , David Sands, A Per Model of Secure Information Flow in Sequential Programs, Higher-Order and Symbolic Computation, v.14 n.1, p.59-91, March 2001
	David A. Schmidt, Induction, Domains, Calculi: Strachey's Contributions to Programming-Language Engineering, Higher-Order and Symbolic Computation, v.13 n.1-2, p.89-101, April 2000
	Paritosh Shroff , Scott F. Smith , Mark Thober, Securing information flow via dynamic capture of dependencies, Journal of Computer Security, v.16 n.5, p.637-688, November 2008
	Dorina Ghindici , Gilles Grimaud , Isabelle Simplot-Ryl, Embedding verifiable information flow analysis, Proceedings of the 2006 International Conference on Privacy, Security and Trust: Bridge the Gap Between PST Technologies and Business Services, October 30-November 01, 2006, Markham, Ontario, Canada
	Kohei Honda , Nobuko Yoshida, A uniform type structure for secure information flow, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.6, p.31-es, October 2007
	Lantian Zheng , Andrew C. Myers, Securing nonintrusive web encryption through information flow, Proceedings of the third ACM SIGPLAN workshop on Programming languages and analysis for security, June 07-13, 2008, Tucson, AZ, USA
	Alejandro Russo , Koen Claessen , John Hughes, A library for light-weight information-flow security in haskell, Proceedings of the first ACM SIGPLAN symposium on Haskell, September 25-25, 2008, Victoria, BC, Canada
	Limin Jia , Steve Zdancewic, Encoding information flow in Aura, Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, June 15-21, 2009, Dublin, Ireland
	Horatiu Cirstea , Pierre-Etienne Moreau , Anderson Santana de Oliveira, Rewrite Based Specification of Access Control Policies, Electronic Notes in Theoretical Computer Science (ENTCS), 234, p.37-54, March, 2009
	Thomas H. Austin , Cormac Flanagan, Efficient purely-dynamic information flow analysis, Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, June 15-21, 2009, Dublin, Ireland
	Ana Almeida Matos , Gérard Boudol, On declassification and the non-disclosure policy, Journal of Computer Security, v.17 n.5, p.549-597, October 2009
	William L. Harrison , James Hook, Achieving information flow security through monadic control of effects, Journal of Computer Security, v.17 n.5, p.599-653, October 2009