ANKUR TALY
About Me
Hi, I am Ankur Taly, 2nd 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. My email address is ataly AT cs.stanford.edu
Interests
I am broadly interested in the application of Formal methods to Verification and Security. Concretely, here is the current list (keeps growing) :
- JavaScript, Web Security
- Deductive techniques for Verification and Synthesis, Abstract Interpretation
- Formal Semantics of programming languages
- ...
Lab Activities
I am coordinator of the Stanford Security Seminar which occurs approximately on alternative 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
- Javascript Security (with Prof. John C. Mitchell and Dr. Sergio Maffeis) : This work revolves around analysing and proving security properties for JavaScript based web security mechanisms and designing provable safe isolation mechanisms for untrusted Javascript code. As a first step towards setting a framework for analysing JavaScript, we formalized the operational semantics for the entire ECMA-262 standard.
- 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 (Accepted and currently submitted)
- Deductive Verification of Continuous Dynamical Systems - Ankur Taly, Ashish Tiwari
- accepted at FSTTCS 2009
- Isolating JavaScript with Filters, Rewriting, and Wrappers
- Sergio Maffeis, John C. Mitchell, Ankur Taly - accepted at ESORICS 2009 PDF
- Run-Time Enforcement of Secure JavaScript Subsets
- Sergio Maffeis, John C. Mitchell, Ankur Taly - in W2SP 2009
PDF
- Language based Isolation of Untrusted JavaScript - Sergio Maffeis, Ankur Taly - in Proc. of CSF 2009
PDF
- Synthesizing Switching Logic using Constraint Solving - Ankur Taly, Ashish Tiwari, Sumit Gulwani - in Proc. of VMCAI 2009 PDF
- An Operational Semantics for JavaScript - Sergio Maffeis, John C. Mitchell, Ankur Taly - in Proc. of APLAS 2008
PDF
- Static Analysis by Policy Iteration on Relational domains - Stephane Gaubert, Eric Goubault, Ankur Taly, Sarah Zennou - in Proc. ESOP 2007 PDF
- Efficient Symbolic Reachability of Networks of Transition Systems - Sudeep Juvekar, Ankur Taly, Varun Kanade, Supratik Chakraborty - in General Motors Workshop on Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems, Bangalore (2007) PDF
Talks
- 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