|
Avik Chaudhuri Software Engineer, Facebook [CV | Research Statement | Projects | Papers | Software] |
My research interests span the areas of programming languages and computer security. I have recently joined the HipHop Team at Facebook. Previously, I was a member of the Programming Language Research Group at Adobe Systems, where I focused on the future of the ActionScript language and the Flash platform, and for a while, served on the JavaScript standardization committee.
Prior to joining the industry, I worked in the Programming Languages group at UMD as a post-doctoral research associate with Jeffrey Foster. Between 2004 and 2008 I earned 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. In between, I have spent various summers at MSR, NICTA, and INRIA.
Professional Activities
Program committee member ESOP 2014, STOP 2012, PLAS 2012, CCS 2011, PLAS 2010, FMSE 2008
External review committee member POPL 2013
Research
Projects (see also here)
| ActionScript Language Specification [work at Adobe] | |
| ActionScript is the core scripting language in which Flash applications are developed. While its roots lie in JavaScript, there are several features in ActionScript that go beyond JavaScript (e.g., class-based inheritance, namespaces, strict-mode compilation, application domains). Unfortunately, the only "specification" of ActionScript has been its implementation, which means that some aspects of the language remain arcane, and any bugs in the implementation cause backward-compatibility problems. We have developed a rigorous definitive specification of the syntax and semantics of ActionScript programs. | |
| Gradual Type Inference for ActionScript [work at Adobe] | |
| ActionScript enforces a combination of static and dynamic checks on programs, but it is unclear what such checks guarantee. Furthermore, there is no type inference in ActionScript. In the past, we have studied the impact of optional type information on dynamic compilation of ActionScript bytecode (DLS 2011). Recently we are working towards a new gradual type system for ActionScript with the following main design intentions: (1) reconciling type inference with static types (annotations) and the dynamic type (*) via the notion of "unsafe" code regions; (2) providing meanings to types via a combination of static and dynamic checks that provably restrict runtime errors to unsafe code regions; and (3) optimizing code by eliminating dynamic checks wherever they are subsumed by static checks. Along these lines, we have developed a new type inference algorithm that can improve the performance of gradually typed programs without introducing any new run-time failures (POPL 2012). | |
| Specification and Verification of Ruby Programs [post-doctoral 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 typing to catch various run-time errors in Rails applications (ASE 2009). More recently, we have implemented a programmable, automated engine for symbolically analyzing security properties of Rails applications (CCS 2010). We are now exploring advanced static and dynamic techniques for precise and tractable type inference of Ruby programs. In particular we have developed a new technique for dynamic inference of static types (POPL 2011). | |
| Language-Based Security on Android [work in progress] | |
| 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 [doctoral 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 (see also here)
| [12/12] | Types and Access Controls for Cross-Domain Security on Flash [with Aseem Rastogi and Rob Johnson] Proc. 10th Asian Symposium on Programming Languages and Systems, Kyoto, Japan (APLAS 2012), pp. 82-97. |
| [01/12] | The Ins and Outs of Gradual Type Inference [with Aseem Rastogi and Basil Hosmer] Proc. 39th ACM Symposium on Principles of Programming Languages, Philadelphia, USA (POPL 2012), pp. 481-494. [Abstract+BibTeX] |
| [10/11] | The Impact of Optional Type Information on JIT Compilation of Dynamically Typed Languages [with Mason Chang, Bernd Mathiske, Edwin Smith, Andreas Gal, Michael Bebenita, Christian Wimmer, and Michael Franz] Proc. 7th ACM Symposium on Dynamic Languages, Portland, USA (DLS 2011), pp. 13-24. [Abstract+BibTeX] (© ACM) |
| [01/11] | Dynamic Inference of Static Types for Ruby [with David An, Jeffrey Foster, and Michael Hicks] Proc. 38th ACM Symposium on Principles of Programming Languages, Austin, USA (POPL 2011), pp. 459-472. Follow-up position paper to appear in Proc. International Workshop on Scripts to Programs (STOP 2011). [Abstract+BibTeX] (© ACM) |
| [10/10] | Symbolic Security Analysis of Ruby-on-Rails Web Applications [with Jeffrey Foster] Proc. 17th ACM Conference on Computer and Communications Security, Chicago, USA (CCS 2010), pp. 585-594. [Abstract+BibTeX] (© ACM) |
| [02/10] | Liberalizing Dependency Technical Report arXiv:1004.1211, Computing Research Repository. [Abstract] |
| [11/09] | SCanDroid: Automated Security Certification of Android Applications [with Adam Fuchs and Jeffrey Foster] In preparation. [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), pp. 590-594. [Abstract+BibTeX] (© IEEE) |
| [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
| Rubydust [with David An, Jeffrey Foster, and Michael Hicks] | |
| Rubydust is an implementation of a new technique for dynamic type inference in Ruby, described in (POPL 2011). It is written in Ruby itself, as a library, exploiting Ruby's powerful dynamic features for introspection. It has been used to find type errors as well as to infer useful types for Ruby programs. | |
| Rubyx [with Jeffrey Foster] | |
| 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, as described in (CCS 2010). | |
| 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 Prasad Naldurg, Sriram Rajamani, Ganesan Ramalingam, and Subbu Velaga] | |
| 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 MPK 14.03
Email avik@fb.com
Postal mail
1 Hacker Way
Menlo Park, CA 94025