|
Avik Chaudhuri Post-doctoral fellow University of Maryland at College Park [CV | Research Statement | Projects | Papers | Software] |
My research interests lie at the intersection of computer security, programming languages, and logic. In 2009 I joined the Programming Languages group at UMD as a research associate with Jeffrey Foster. Between 2004 and 2008 I completed 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 PLAS 2010, FMSE 2008
Research
Projects
| Specification and Verification of Ruby Programs [ongoing work] | |
| 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 (ASE 2009). More recently, we have formalized an operational semantics for Ruby, and are exploring a combination of static typing and symbolic analysis to verify complex correctness properties of Ruby programs, including security properties of Rails applications. | |
| Language-Based Security on Android [ongoing work] | |
| 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 (PLAS 2009). More recently, we have implemented an automatic security certifier for Android applications based on an extension of this work, described here. | |
| Foundations of Access Control for Systems Security [dissertation work] | |
| Protection in systems is typically implemented via access control, but access control seldom implies security per se. In the past, 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 (PLAS 2008, CCS 2008); we have found serious attacks on a cryptographic file system protocol using an automatic theorem prover (S&P 2008); we have shown how to implement access control securely in distributed settings (FCS-ARSPA-WITS 2008, FORTE 2006, FMSE 2005); and we have invented language-based techniques that combine static typing and dynamic access checks to verify dynamic security specifications in such systems (CONCUR 2006, CSF 2006). Recently, we have applied some of these ideas to provide language support for proof-carrying authorization systems (ESORICS 2009). A comprehesive account of this line of work can be found in my dissertation. |
Papers
| [11/09] | SCanDroid: Automated Security Certification of Android Applications [with Adam Fuchs and Jeffrey Foster] Submitted to S&P 2010. [Abstract] |
| [11/09] | Static Typing for Ruby on Rails [with David An and Jeffrey Foster] Proc. 24th IEEE/ACM Conference on Automated Software Engineering, Auckland, New Zealand (ASE 2009), to appear. [Abstract] |
| [10/09] | Liberalizing Dependency Submitted to ESOP 2010. [Abstract] |
| [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), pp. 184-199. [Abstract+BibTeX] (© Springer) |
| [08/09] | A Concurrent ML Library in Concurrent Haskell Proc. 14th ACM International Conference on Functional Programming, Edinburgh, Scotland (ICFP 2009), pp. 269-280. [Abstract+BibTeX+Implementation] (© ACM) |
| [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+BibTex+Talk] (© ACM) |
| [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 Subbu 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. [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 Symposium/Workshop, Venice, Italy (CSF 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. |
Software
| Rubyx [with Jeffrey Foster and David An, in progress] | |
| Rubyx is a symbolic analysis engine for Ruby, written in OCaml, with in-built support for specification and verification of scripts using object invariants, dependent types, and induction over data structures. In particular, it has been used to prove complex security and correctness properties of web applications developed with Ruby on Rails. | |
| SCanDroid [with Adam Fuchs and Jeffrey Foster] | |
| SCanDroid is an automatic security certifier for mobile applications run on Android, described here. It is written in Java, using the WALA framework to implement a static information-flow security analysis based on the method proposed in (PLAS 2009). | |
| DRails [with David An and Jeffrey Foster] | |
| DRails translates web applications developed with Ruby on Rails to pure Ruby code that can be typechecked using DRuby (a static type inference system for Ruby). The translator, described in (ASE 2009), is written partly in OCaml and partly in Ruby using a combination of static and dynamic code generation techniques. | |
| PCAL [with Deepak Garg] | |
| PCAL is a compiler for a Bash-like language that automates proof management for scripts interacting with a PCA system interface, as described in (ESORICS 2009). The current implementation, written in SML, works in conjunction with PCFS (a proof-carrying file system) and a theorem prover for Binder Logic (an authorization logic with support for explicit time and state). | |
| CML/CH [supported by Benjamin Franksen] | |
| CML/CH is a library that implements Concurrent ML-style primitives over core Concurrent Haskell, while remaining faithful to the standard semantics of those primitives, as described in (ICFP 2009). | |
| EON [with Subbu Velaga, Prasad Naldurg, Ganesan Ramalingam, and Sriram Rajamani] | |
| EON is a query evaluation engine, written in F#, for a dynamic logic programming language proposed in (CCS 2008). It has been used to study security models of various operating systems, and to analyze security properties of applications designed to run on such systems. | |
| StrEd [with Gérard Huet] | |
| StrEd is a structured editor, written in OCaml, for building well-typed programs from arbitrary ML type signatures; it runs on a CGI-based transaction manager that allows distributed editing. |
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)