|
Avik Chaudhuri Post-doctoral fellow University of Maryland at College Park [CV | Research Statement | Projects | Papers] |
My research interests lie at the intersection of computer security, programming languages, and logic. Recently I joined the Programming Languages group at UMD as a research associate with Jeffrey Foster, after completing a PhD under the tutelage of Martín Abadi. Further back, I did undergraduate studies in Computer Science and Engineering at IIT Delhi, where I was advised by Sanjiva Prasad.
Professional Activities
Program committee member FMSE 2008
Research
Projects
| Specification and Verification of Ruby Programs | |
| Ruby is a dynamically-typed object-oriented scripting language, which is at the heart of Rails, a widely popular web-application framework. Our goal is to develop techniques for analyzing the correctness of Ruby programs, including web applications written in Rails. In preliminary work we have applied static type inference to catch various run-time errors in Rails applications [ACF09]. More recently, we have formalized an operational semantics for Ruby, and are exploring a combination of static typing and symbolic analysis to verify finer correctness properties of Ruby programs, including security properties of Rails applications. | |
| Language-Based Security on Android | |
| Android is Google's new open-source platform for mobile devices, which includes an SDK that provides the tools and APIs necessary to develop applications for the platform in Java. By design, such applications can share their components with other applications on the platform, in certain controlled ways. Our goal is to support certified installation of secure Android applications, borrowing ideas from proof-carrying code. In preliminary work we have formalized an operational semantics and a security type system for an abstract idealization of the Android SDK [C09b]. We are currently implementing a security verifier for Android applications based on an extension of this work. | |
| Foundations of Access Control for Systems Security | |
| Protection in systems is typically implemented via access control, but access control seldom implies security per se. In past work, we have studied the formal implications of access control for security in operating systems such as Windows Vista and Asbestos, file systems such as OSDFS and Plutus, and other distributed systems. In particular, we have implemented techniques based on type inference and query evaluation to analyze information-flow properties of label-based operating systems [CNR08, CNRRV08]; we have found serious attacks on a cryptographic file system protocol using an automatic theorem prover [BC08]; we have derived secure distributed implementations of access control with capabilities [C08a, CA06, CA05]; and we have invented language-based techniques that combine static typing and dynamic access checks to verify dynamic security specifications in such systems [C06, CA06]. Recently, we have applied some of these ideas to provide language support for a file system based on proof-carrying authorization [CG09]. |
Papers
| [09/09] | PCAL: Language Support for Proof-Carrying Authorization Systems [with Deepak Garg] Proc. 14th European Symposium on Research in Computer Security, Saint Malo, France (ESORICS 2009), to appear. [Abstract] |
| [08/09] | A Concurrent ML Library in Concurrent Haskell Proc. 14th ACM International Conference on Functional Programming, Edinburgh, Scotland (ICFP 2009), to appear. [Abstract+BibTeX+Implementation] |
| [06/09] | Language-Based Security on Android Proc. 4th ACM Workshop on Programming Languages and Analysis for Security, Dublin, Ireland (PLAS 2009), pp. 1-7. [Abstract+Talk] (© ACM) |
| [05/09] | Static Typing for Ruby on Rails [with David An and Jeffrey Foster] Submitted to ASE 2009. [Abstract] |
| [12/08] | Foundations of Access Control
for Secure Storage PhD Dissertation, University of California, Santa Cruz, USA. [Abstract+Talk] |
| [10/08] | EON: Modeling and Analyzing Dynamic Access
Control Systems with Logic Programs [with Prasad Naldurg, Ganesan Ramalingam, Sriram Rajamani, and Lakshmisubrahmanyam Velaga] Proc. 15th ACM Conference on Computer and Communications Security, Alexandria, USA (CCS 2008), pp. 381-390. [Abstract+BibTeX+Implementation] (© ACM) |
| [06/08] | On Secure
Distributed Implementations of Dynamic Access Control Proc. LICS/CSF Joint Workshop on Computer Security, Pittsburgh, USA (FCS-ARSPA-WITS 2008), pp. 93-107. (Also submitted to Journal of Automated Reasoning.) [Abstract+BibTeX+Technical report] |
| [06/08] | A Type System for
Data-Flow Integrity on Windows Vista [with Sriram Rajamani and Prasad Naldurg] Proc. 3rd ACM Workshop on Programming Languages and Analysis for Security, Tucson, USA (PLAS 2008), pp. 89-100. (Also appears in ACM SIGPLAN Notices, 43(12):9-20, as one of "the top two papers of PLAS 2008".) [Abstract+BibTeX+Technical report] (© ACM) |
| [05/08] | Automated Formal
Analysis of a Protocol for Secure File Sharing on Untrusted
Storage [with Bruno Blanchet] Proc. 29th IEEE Symposium on Security and Privacy, Oakland, USA (S&P 2008), pp. 417-431. [Abstract+BibTeX+Implementation] (© IEEE) |
| [01/07] | Foundations of
Access Control for Secure Storage PhD Dissertation Proposal, University of California, Santa Cruz, USA. |
| [09/06] | Formal Analysis of Dynamic, Distributed
File-System Access Controls [with Martín Abadi] Proc. 26th IFIP Conference on Formal Methods for Networked and Distributed Systems, Paris, France (FORTE 2006), pp. 99-114. [Abstract+BibTeX] (© Springer) |
| [08/06] | Dynamic Access Control in a Concurrent Object Calculus Proc. 17th International Conference on Concurrency Theory, Bonn, Germany (CONCUR 2006), pp. 263-278. [Abstract+BibTeX] (© Springer) |
| [07/06] | Secrecy by Typing and File-Access Control [with Martín Abadi] Proc. 19th IEEE Computer Security Foundations Workshop, Venice, Italy (CSFW 2006), pp. 112-123. [Abstract+BibTeX] (© IEEE) |
| [11/05] | Formal
Security Analysis of Basic Network-Attached Storage [with Martín Abadi] Proc. 3rd ACM Workshop on Formal Methods in Security Engineering, Fairfax, USA (FMSE 2005), pp. 43-52. [Abstract+BibTeX] (© ACM) |
| [07/04] | A Generic
Automated Proof-Carrying
Framework Master's Thesis, Indian Institute of Technology, New Delhi, India. |
| [05/04] | Validation of Mobile Code under Transformations [with Sanjiva Prasad] Technical Report, Indian Institute of Technology, New Delhi, India. |
| [12/03] | Symbolic Forced Simulation: Interface Generation for Systems-on-Chip [with Arcot Sowmya and Sethu Ramesh] Technical Report, University of New South Wales, Sydney, Australia. |
| [05/03] | Polytypic Structured Editing [with Sanjiva Prasad] Technical Report, Indian Institute of Technology, New Delhi, India. |
| [07/02] | A Distributed Structured Editor for ML [with Gérard Huet] Technical Report, Institut National de Recherche en Informatique et Automatique, Rocquencourt, France. |
Contact
Office AVW 4165
Email avik@cs.umd.edu
Phone 1.301.405.3593 (office)
Postal mail
Department of Computer Science
University of Maryland
A. V. Williams Building
College Park, MD 20742
Fax 1.301.403.4524 (online)