About Me
Current Research
Publications
Selected Talks
About Me
Hi, I am Ankur Taly, Research Scientist in the Security Research group at Google. Prior to joining Google, I was a PhD candidate in the Dept. of Computer Science at Stanford University, advised by Prof. John C. Mitchell. Before coming to Stanford, I spent four wonderful years at Indian Institute of Technology (IIT), Bombay where I completed my B.Tech in Computer Science and Engg.
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:
- I am now a Research Scientist in the Security Research group at Google.
- 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 no longer the coordinator of the Stanford Security Seminar.
Kindly send an email to Joe Zimmerman if you would like to give a talk.
PC Participation
HOTSPOT 2013,
PLAS 2013,
POST 2014
Please consider submitting a paper to these venues.
Research Themes
- Securing Bearer-Token based Authorization frameworks (at Google)
- Semantics for JavaScript
- Javascript Sandboxing (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
Proc. of PLDI 2012 PDF
- 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