Papers, Talks and Recent Manuscripts

Research partially supported by National Science Foundation grants EIA-9806835, CCR-0209205, CCR-0296182, ITR-0326577, CNS-0627748; EPSRC grant GR/S03539; IBM T.J. Watson Research Center; Microsoft Research.
Co-authors: Martín Abadi, Torben Amtoft, Sruthi Bandhakavi, Mike Barnett, Matthew B. Dwyer, Roberto Giacobazzi , John Hatcliff, Nevin Heintze, Thomas Jensen, Gurvan Le Guernic , Ben Livshits , Isabella Mastroeni , David A. Naumann, Aditya Nori, Marco Pistoia , Sriram Rajamani, Venkatesh P. Ranganath, Jon G. Riecke, Stan Rosenberg, David A. Schmidt, Qi Sun

Access control, information flow and security

Benjamin Livshits, Aditya Nori, Sriram Rajamani and Anindya Banerjee
Merlin: Specification Inference for Explicit Information Flow Problems.
In 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) , pp. 75--86, June 2009. PDF; ACM Press. Last revised, March 2009.

Avraham Shinnar, Marco Pistoia and Anindya Banerjee.
A Language for Information Flow: Dynamic Tracking in Multiple Interdependent Dimensions.
In Proceedings of 2009 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS) , pp. 125--131, June 2009. PDF; ACM Press. Last revised, May 2009. Research Report, RC 2451 IBM TJ Watson Research Center. Last revised, April 2008.

Anindya Banerjee, David A. Naumann and Stan Rosenberg.
Expressive Declassification Policies and their Modular Static Enforcement.
In Proceedings of the 2008 IEEE Symposium on Security and Privacy (S& P) , pp. 339--353, May 2008. IEEE Computer Society Press. PDF; Last revised, March 2008.
Torben Amtoft and Anindya Banerjee.
Verification Condition Generation for Conditional Information Flow.
In Fifth ACM Workshop on Formal Methods in Security Engineering (FMSE) , pp. 2--11, November 2007. ACM Press. PDF; Last revised, June 2007. KSU CIS TR-2007-2; Last revised, June 2007.
Anindya Banerjee, David A. Naumann and Stan Rosenberg.
Towards a Logical Account of Declassification (Short Paper).
In Proceedings of the 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS) , pp. 61--65, June 2007. ACM Press. PDF; Last revised, May 2007.
Marco Pistoia, Anindya Banerjee and David A. Naumann
Beyond stack inspection: A unified access-control and information-flow security model.
In Proceedings of the 2007 IEEE Symposium on Security and Privacy (S& P), pp. 149--163, May 2007.
IEEE Computer Society Press. PDF. Last revised, March 2007.
Anindya Banerjee, Roberto Giacobazzi and Isabella Mastroeni.
What you lose is what you leak: Information leakage in declassification policies.
In Proceedings of the Twenty-Third Conference on Mathematical Foundations of Programming Semantics (MFPS), pp. 47-66, volume 173 of Electronic Notes in Theoretical Computer Science, Elsevier, B.V., April 2007. PDF; Last revised, February 2007.
Gurvan Le Guernic, Anindya Banerjee, Thomas Jensen and David A. Schmidt.
Automata-based Confidentiality Monitoring.
In Proceedings of the Eleventh Annual Asian Computing Science Conference(ASIAN). Lecture Notes in Computer Science, Vol. 4435, pp. 75--89, December 2006. Springer.
Anindya Banerjee and David A. Naumann.
A Logical Account of Secure Declassification. PDF; Last revised, April 2006.
Superceded by PLAS 2007 and S& P 2008 papers.
Torben Amtoft, Sruthi Bandhakavi and Anindya Banerjee.
A Logic for Information Flow in Object-Oriented Programs.
In Proceedings of the Thirty-third Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 91-102, January 2006. Talk at POPL; PDF; Last revised, November 2005; Technical Report, KSU CIS-TR-2005-1; Last revised, August 2006.
Anindya Banerjee and David A. Naumann.
Stack-based Access Control and Secure Information Flow.
Journal of Functional Programming 15(2), pp. 131-177, Special issue on Language-based Security, March 2005.
PDF; Dagstuhl Seminar 03411 talk.
Note:This paper supercedes the CSFW 2003 and CSFW 2002 papers below.
Torben Amtoft and Anindya Banerjee.
A Logic for Information Flow Analysis with an Application to Forward Slicing of Simple Imperative Programs.
PDF; Science of Computer Programming 64(1), pp. 3-28, January 2007.
Supercedes the SAS 2004 paper Information Flow Analysis in Logical Form.
Anindya Banerjee and David A. Naumann.
History-based Access Control and Secure Information Flow.
In Proceedings of the workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Cards (CASSIS), pp. 27-48, volume 3362 of Lecture Notes in Computer Science, Springer-Verlag, March 2005.
PDF (© Springer-Verlag)
Torben Amtoft and Anindya Banerjee
Information flow analysis in logical form.
In Proceedings of the Eleventh International Static Analysis Symposium (SAS) , pp. 100-115, volume 3148 of Lecture Notes in Computer Science, Springer-Verlag, August 2004. PDF (© Springer-Verlag)
Technical Report KSU CIS-TR-2004-3. Last revised, May 2004.
Qi Sun, Anindya Banerjee and David A. Naumann
Modular and constraint-based information flow inference for an object-oriented language.
In Proceedings of the Eleventh International Static Analysis Symposium (SAS) , pp. 84-99, volume 3148 of Lecture Notes in Computer Science, Springer-Verlag, August 2004. PDF (© Springer-Verlag). Last revised, May 2004.
Anindya Banerjee and David A. Naumann.
Using Access Control for Secure Information Flow in a Java-like Language.
In Proceedings of the Sixteenth IEEE Computer Security Foundations Workshop (CSFW) , pp. 155-169, June 2003.
IEEE Computer Society Press. PDF. CSFW'03 talk.
Anindya Banerjee and David A. Naumann.
Secure Information Flow and Pointer Confinement in a Java-like Language.
In Proceedings of the Fifteenth IEEE Computer Security Foundations Workshop (CSFW) , pp. 253-267, June 2002.
IEEE Computer Society Press. PDF. CSFW'02 talk. Pointerfest talk
Martín Abadi, Anindya Banerjee, Nevin Heintze and Jon G. Riecke.
A Core Calculus of Dependency.
In Proceedings of the Twenty-sixth Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 147-160, January 1999. ACM Press. PS

Pointer confinement and data abstraction

Anindya Banerjee and David A. Naumann.
A Logical Account of Hoare's Mismatch: Information Hiding via Second Order Framing in Region Logic.
PDF; Last revised, July 2009.
Anindya Banerjee, Mike Barnett and David A. Naumann.
Boogie Meets Regions: a Verification Experience Report.
In Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08), Lecture Notes in Computer Science, Vol. 5295, pp. 177--191, October 2008. Springer. PDF; Technical Report MSR-TR-2008-79; Last revised, May 2008.
Download Boogie PL code for examples in paper.
Anindya Banerjee, David A. Naumann and Stan Rosenberg.
Regional Logic for Local Reasoning about Global Invariants.
In Proceedings of the Twenty-second European Conference on Object-oriented Programming (ECOOP) , pp. 387-411, volume 5142 of Lecture Notes in Computer Science, Springer-Verlag, July 2008. PDF; Last revised, May 2008.
Anindya Banerjee and David A. Naumann.
State based ownership, reentrance, and encapsulation.
In Proceedings of the Nineteenth European Conference on Object-oriented Programming (ECOOP) , pp. 387-411, volume 3586 of Lecture Notes in Computer Science, Springer-Verlag, July 2005.
PDF; Last revised, May 2005.
Anindya Banerjee and David A. Naumann.
State based encapsulation and generics.
PDF; Technical Report, CS-2004-11, Stevens Institute of Technology and KSU CIS-TR-2004-5. Last revised, December 2004.
Anindya Banerjee and David A. Naumann.
Ownership transfer and abstraction.
PDF; Technical Report, KSU CIS-TR-2004-1. Last revised, October 2003.
Note:This paper supercedes the following FTfJP 2003 paper.
Anindya Banerjee and David A. Naumann.
Ownership: transfer, sharing, and encapsulation.
In ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP) , July 2003.
PDF.
Anindya Banerjee and David A. Naumann.
Ownership Confinement Ensures Representation Independence in Object-Oriented Programs.
Journal of the ACM 52(6), pp. 894-960, November 2005.
PDF; Technical Report KSU CIS-TR-2004-6 and SIT CS-TR-2004-14.
This supercedes the following POPL version, improving and extending it to include a static analysis and substantial examples.
Anindya Banerjee and David A. Naumann.
Representation independence, Confinement, and Access Control.
In Proceedings of the Twenty-ninth Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 166-177, January 2002.
ACM Press. PDF (Extended Abstract with appendices).

Program analysis and Program transformations

Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, Matthew B. Dwyer and John Hatcliff.
A New Foundation for Control-Dependence and Slicing for Modern Program Structures.
ACM Transactions on Programming Languages and Systems (TOPLAS) 29(5), August 2007.
Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, Matthew B. Dwyer and John Hatcliff.
A New Foundation for Control-Dependence and Slicing for Modern Program Structures.
In Proceedings of the European Symposium of Programming (ESOP) , April 2005. Lecture Notes in Computer Science, Vol. 3444, pp. 77--93.
PDF (© Springer-Verlag); Technical Report, TR-2004-8, SAnToS Laboratory. Last revised, October 2004.
Anindya Banerjee and Thomas Jensen.
Modular Control-flow Analysis with Rank 2 Intersection Types.
Mathematical Structures in Computer Science 13(1), pp. 87-124, February 2003.
Cambridge University Press. PDF (Preprint)
Note:This paper supercedes the following ICFP 1997 paper.
Anindya Banerjee, Nevin Heintze and Jon G. Riecke.
Design and Correctness of Program Transformations based on Control-flow Analysis.
Invited paper, Proceedings of the International Symposium on Theoretical Aspects of Computer Software (TACS), pp. 420-447, volume 2215 of Lecture Notes in Computer Science, Springer-Verlag, October 2001. PS (© Springer-Verlag). Last revised September 2001.
Anindya Banerjee, Nevin Heintze and Jon G. Riecke.
Region Analysis and the Polymorphic Lambda Calculus.
In Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS) , pp. 88-97, July 1999.
IEEE Computer Society Press. PS (Extended abstract)
Anindya Banerjee and David A. Schmidt.
Stackability in the Simply-Typed Call-by-Value Lambda Calculus.
Science of Computer Programming, Volume 31, pp. 47-73, 1998. PS (Preprint)
Note:This paper supercedes the following SAS 1994 paper.
Anindya Banerjee.
A Modular, Polyvariant and Type-based Closure Analysis.
In Proceedings of the Second ACM International Conference on Functional Programming (ICFP), pp. 1-10, June 1997. ACM Press. PS
Anindya Banerjee and David A. Schmidt.
Stackability in the Simply-Typed Call-by-Value Lambda Calculus.
In Proceedings of the First International Static Analysis Symposium (SAS), pp. 136-151, volume 864 of Lecture Notes in Computer Science, Springer-Verlag, September 1994. PS (© Springer-Verlag)

Miscellaneous papers and thesis

Anindya Banerjee and David A. Naumann.
A Static Analysis for Instance-based Confinement in Java.
PDF; Extended version. Last revised November 2001.
Anindya Banerjee and David A. Naumann.
A Simple Semantics and Static Analysis for Java Security.
Technical Report 2001-1, Stevens Institute of Technology, July 2001. PDF
Anindya Banerjee.
The Semantics and Implementation of Bindings in Higher-Order Programming Languages.
Ph.D. thesis, Department of Computing and Information Sciences, Kansas State University,1995.
Anindya Banerjee and David A. Schmidt.
A Categorical Interpretation of Landin's Correspondence Principle.
In Proceedings of the Ninth Conference on Mathematical Foundations of Programming Semantics (MFPS), pp. 587-602, volume 802 of Lecture Notes in Computer Science, Springer-Verlag, 1994. PS (© Springer-Verlag)