About Me
Current Research
Publications
Selected Talks
About Me
Hi, I am Ankur Taly, 5th year Ph.D candidate in the Dept. of Computer Science at Stanford University. My research advisor is Prof. John C. Mitchell. Prior to joining Stanford, I completed my B.Tech in Computer Science and Engg. from Indian Institute of Technology (IIT), Bombay in 2007.
Email: ataly AT stanford.edu
Research Interests: Formal Methods in general. Currently,
- Applications of: Logic, Programming Language Theory, Constraint Solving,...
- To: Web Security, Hybrid Systems, Program Verification, Synthesis,...
Curriculum Vitae:
PDF
Recent:
- My MSR internship work (with Patrice Godefroid) on automated synthesis of processor instruction encodings got accepted at PLDI'12!
- 3rd place at the AT&T Best Applied Security Paper Award competition, for the API Confinement paper (published at S&P 2011)
- Interned at MSR Redmond with Patrice Godefroid during June-Sept 2011 and worked on automated synthesis of symbolic instruction encodings from I/O samples
- My Encapsulation Analysis paper got into S&P 2011
- Interned at Google with the Caja group from June-Sept 2010
- Received the 2010 Google Phd Fellowship in Language Security
- Passed the Theory Quals: worked on Separation Logic, see report
I am the coordinator of the Stanford Security Seminar which occurs approximately on alternate tuesdays at 4:30 pm in the Gates building, 4B center area . Do send me an email if you are interested in giving a talk.
Current Research
- Automated Analysis of Security-critical Javascript APIs (with the Google Caja group): The goal of this project is to design automated and provably-sound techniques for analysing security-JavaScript APIs for verifying various properties such as confinement, correctness and defensive consistency (see our Oakland 2011 paper for results on confinement analysis).
- Formalising the Object Capability model (with Prof. John C. Mitchell and Dr. Sergio Maffeis): The goal of this project is to come up with a formal model (using the semantics of the underlying language) for object capability based systems and formally state the security properties associated with them. Once this is accomplished, we intend to use the model for proving correctness of the Google Caja framework (see our Oakland 2010 paper).
- Separation Logic and the Mashup Isolation Problem: This work revolves around using variants of separation logic for verifying heap isolation between different components of a web mashup. This work was started during my qualifier exam in theoretical computer science (see report).
- Semantics for JavaScript
- Javascript Security (with Prof. John C. Mitchell and Dr. Sergio Maffeis): This work revolves around designing and analyzing provably-secure language-based mechanisms for sandboxing untrusted JavaScript
- Hybrid Systems Verification (with Dr. Ashish Tiwari): This work revolves around formulating deductive techniques for synthesis and verification of hybrid systems. My current problem is to formulate a sound and complete rule for safety verification of continuous dynamical systems.
Publications
- Language-based security, Web Security
- Automated Analysis of Security-critical JavaScript APIs - Ankur Taly, Ulfar Erlingsson, Mark S. Miller, John C. Mitchell, Jasvir Nagra
Accepted at IEEE Security & Privacy (Oakland conference) 2011 PDF
-
Object Capabilities and Isolation of Untrusted Web Applications- Sergio Maffeis, John C. Mitchell, Ankur Taly
Proc. of IEEE Security & Privacy (Oakland conference) 2010 PDF
- Isolating JavaScript with Filters, Rewriting, and Wrappers
- Sergio Maffeis, John C. Mitchell, Ankur Taly
Proc. of ESORICS 2009 PDF
- Run-Time Enforcement of Secure JavaScript Subsets
- Sergio Maffeis, John C. Mitchell, Ankur Taly
W2SP 2009
PDF
- Language based Isolation of Untrusted JavaScript - Sergio Maffeis, Ankur Taly
Proc. of CSF 2009
PDF
- An Operational Semantics for JavaScript - Sergio Maffeis, John C. Mitchell, Ankur Taly
Proc. of APLAS 2008
PDF
- Static Analysis, Verification, Synthesis
- Automated Synthesis of Symbolic Instruction Encodings from I/O samples -Patrice Godefroid, Ankur Taly
Accepted at PLDI 2012
- Synthesizing Switching Logic using Constraint Solving - Ankur Taly, Ashish Tiwari, Sumit Gulwani
Journal on Software Tools for Technology Transfer (STTT 2011) Springer Link
- Switching Logic Synthesis for Reachability- Ankur Taly, Ashish Tiwari
Proc. of EMSOFT 2010 PDF
- Deductive Verification of Continuous Dynamical Systems - Ankur Taly, Ashish Tiwari
Proc. of FSTTCS 2009 PDF
- Synthesizing Switching Logic using Constraint Solving - Ankur Taly, Ashish Tiwari, Sumit Gulwani
Proc. of VMCAI 2009 PDF
- Static Analysis by Policy Iteration on Relational domains - Stephane Gaubert, Eric Goubault, Ankur Taly, Sarah Zennou
Proc. of ESOP 2007 PDF
- Efficient Symbolic Reachability of Networks of Transition Systems - Sudeep Juvekar, Ankur Taly, Varun Kanade, Supratik Chakraborty
Proc. of General Motors Workshop on Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems, Bangalore (2007) PDF
Selected Talks
- Automated Analysis of Security-critical JavaScript APIs - May'11, IEEE SSP, Oakland, USA PPT
- Object Capabilities and Isolation of Untrusted Web Applications - May'10, IEEE SSP, Oakland, USA PDF
- Separation Logic and the Mashup Isolation Problem - April'10, Stanford, USA PDF
- Deductive Verification of Continuous Dynamical Systems - Dec'09, FSTTCS, Kanpur, India PDF
- Isolating JavaScript with Filters, Rewriting, and Wrappers - Dec'09, Microsoft Research Bangalore, India PDF
- Language based Isolation of Untrusted JavaScript - July'09, CSF, Port Jefferson, USA PDF
- Run-time Enforcement of Secure JavaScript Subsets - May'09, W2SP, Oakland, USA PDF
- Synthesizing Switching Logic using Constraint Solving - Jan'09, VMCAI, Savannah, USA PDF
- An Operational Semantics for JavaScript - Dec'08, APLAS, Bangalore, India PDF
- Static Analysis by Policy Iteration on Relational domains - Mar'07, ESOP, Braga, Portugal PDF