Jiaqi Tan

About Me

I am a 4th year PhD student in the Department of Electrical and Computer Engineering at Carnegie Mellon University. My research advisor is Prof. Priya Narasimhan. My research interests are in Computer Security and Program Verification, particularly in ensuring that software is free of security faults using formal techniques such as Interactive Theorem Proving. I am also affiliated with the Parallel Data Laboratory.

Previously, I completed my Bachelor's and Master's in Computer Science at the School of Computer Science at Carnegie Mellon University in 2008 and 2009 respectively. My Bachelor's Honor's Thesis was "RAMS and BlackSheep: Inferring white-box application behavior using black-box techniques" (CMU-PDL-08-103), while my Master's Thesis was "Log-based Approaches to Characterizing and Diagnosing MapReduce Systems" (CMU-CS-09-143).

More details about my work can be found at my Google Scholar page.

Thesis Research

White-box Isolation with Black-box Proofs

The goal of my Ph.D. thesis research is to develop a technique and tool-chain which enables developers to obtain machine-code programs which have isolation (memory and control-flow safety) which is programmer-evident, and which can be formally verified in a fully automatic manner. By programmer-evident, I mean that programmers can observe the safety checks which ensure that their programs have the isolation property, and can observe how these safety checks affect their programs. We make use of Interactive Theorem Proving in HOL (Higher Order Logic), and build on the validated, trustworthy formalization of the ARM Instruction Set Architecture (ISA) developed at Cambridge University to develop a novel logic framework for automatically proving safety properties in unmodified executables. This proof process is fully automated, and does not require programmers to provide annotations, function pre/post-conditions, or invariants in a specialized language.

Previously, isolation has been formally proved for machine-code programs only when the isolation has been provided by opaque techniques such as binary rewriting. However, binary rewriting can change the behavior of programs, and the added safety checks cannot be observed by the programmer. This is a problem in High Assurance software projects, where new behaviors must not be introduced after compilation to ensure that software behaves as developers expect. My thesis research aims to address this problem by proving safety properties in machine-code programs which have not undergone binary rewriting to insert safety checks. As a consequence, safety proofs for such programs may fail, and my logic framework is designed to handle such proof failures. In addition, my tool-chain also utilizes information from the proof failures to help developers achieve isolation in their previously unsafe programs.

Related Publications

  1. AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code
    Jiaqi Tan, Hui Jun Tay, Rajeev Gandhi, and Priya Narasimhan.
    (To Appear) In 14th Asian Symposium on Programming Languages and Systems (APLAS), November 2016. (Preprint)

  2. Poster Abstract: BUFS: Towards Bottom-Up Foundational Security for Software in the Internet-of-Things
    Jiaqi Tan, Rajeev Gandhi, and Priya Narasimhan.
    (To Appear) In 1st IEEE/ACM Symposium on Edge Computing (SEC 2016), October 2016.

  3. PCFIRE: Towards Provable, Preventative Control-Flow Integrity Enforcement for Realistic Embedded Software
    Jiaqi Tan, Hui Jun Tay, Utsav Drolia, Rajeev Gandhi, and Priya Narasimhan.
    (To Appear) In ACM SIGBED International Conference on Embedded Software (EMSOFT), October 2016. (Preprint)

  4. White-box Software Isolation with Fully Automated Black-box Proofs
    Jiaqi Tan, Rajeev Gandhi, and Priya Narasimhan.
    In Formal Methods in Computer-Aided Design (FMCAD) Student Forum, September 2015. (Poster) (Talk slides) Awarded Best Student Forum Contribution.

  5. AUSPICE: Automated Safety Property Verification for Unmodified Executables.
    Jiaqi Tan, Hui Jun Tay, Rajeev Gandhi, and Priya Narasimhan.
    In 7th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), July 2015. (Preprint) (Errata, 17 May 2016)

  6. STOVE: Strict, Observable, Verifiable Data and Execution Models for Untrusted Applications.
    Jiaqi Tan, Rajeev Gandhi, and Priya Narasimhan.
    In 6th IEEE International Conference on Cloud Computing Technology and Science (CloudCom) Doctoral Symposium, December 2014. (Preprint)

  7. STOVEPipe: Observable Access Control of User Data for Untrusted Applications on Mobile Devices.
    Jiaqi Tan, Utsav Drolia, Rolando Martins, Rajeev Gandhi, and Priya Narasimhan.
    In 6th IEEE International Conference on Cloud Computing Technology and Science (CloudCom) (Poster Paper), December 2014. (Preprint)

  8. Poster: Towards Secure Execution of Untrusted Code for Mobile Edge-Clouds.
    Jiaqi Tan, Utsav Drolia, Rajeev Gandhi, and Priya Narasimhan.
    In 7th ACM Conference on Security and Privacy in Wireless and Mobile Networks (WiSec), July 2014. (Preprint)

  9. Challenges in Security and Privacy for Mobile Edge-Clouds.
    Jiaqi Tan, Rajeev Gandhi, Priya Narasimhan.
    Carnegie Mellon University Parallel Data Laboratory Technical Report CMU-PDL-13-113, October 2013.

Other Projects

Mobile and Web Security

Publications

  1. A5: Automated Analysis of Adversarial Android Applications.
    Tim Vidas, Jiaqi Tan, Jayvardhan Nahata, Chaur-Lih Tan, Nicolas Christin, and Patrick Tague.
    In 4th ACM Workshop on Security and Privacy in Smartphones and Mobile Devices (SPSM), November 2014. (Preprint)

  2. Short Paper: CHIPS: Content-based Heuristics for Improving Photo Privacy for Smartphones.
    Jiaqi Tan, Utsav Drolia, Rolando Martins, Rajeev Gandhi, Priya Narasimhan.
    In 7th ACM Conference on Security and Privacy in Wireless and Mobile Networks (WiSec), July 2014. (Preprint)

  3. PETAL: Preset Encoding Table Information Leakage.
    Jiaqi Tan, Jayvardhan Nahata.
    Carnegie Mellon University Parallel Data Laboratory Technical Report CMU-PDL-13-106, April 2013.

Mobile Edge-Cloud Computing

Publications

  1. The next-generation in-stadium experience (keynote). Priya Narasimhan, Utsav Drolia, Jiaqi Tan, Nathan Mickulicz, Priya Narasimhan. In 2015 ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE), Keynote Address.

  2. The Case For Mobile Edge-Clouds. Utsav Drolia, Rolando Martins, Jiaqi Tan, Ankit Chheda, Monil Sanghavi, Rajeev Gandhi, Priya Narasimhan. In 10th IEEE International Conference on Ubiquitous Intelligence and Computing (UIC), December 2013.

Previous Projects

Failure Diagnosis and Visualization for MapReduce Systems

Publications

  1. Theia: Visual Signatures for Problem Diagnosis in Large Hadoop Clusters.
    Elmer Garduno, Soila Kavulya, Jiaqi Tan, Rajeev Gandhi, Priya Narasimhan.
    In USENIX ;login, 38(2), April 2013. (Online article)

  2. Theia: Visual Signatures for Problem Diagnosis in Large Hadoop Clusters.
    Elmer Garduno, Soila Kavulya, Jiaqi Tan, Rajeev Gandhi, Priya Narasimhan.
    In 26th Large Installation System Administration (LISA) Conference, San Diego, CA, Dec 2012.
    Awarded Best Student Paper.

  3. Understanding and Improving the Diagnostic Workflow of MapReduce Users.
    Jason Campbell, Arun Ganesan, Ben Gotow, Soila Kavulya, James Mulholland, Priya Narasimhan, Sriram Ramasubramanian, Mark Shuster, Jiaqi Tan.
    In 5th ACM Symposium on Computer Human Interaction for Management of Information Technology (CHIMIT), Boston, MA, Dec 2011. (Preprint)

  4. Visual, Log-based Causal Tracing for Performance Debugging of MapReduce Systems.
    Jiaqi Tan, Soila Kavulya, Rajeev Gandhi, Priya Narasimhan.
    In 30th IEEE International Conference on Distributed Computing Systems (ICDCS) 2010, Genoa, Italy, Jun 2010. (Preprint)

  5. An Analysis of Traces from a Production MapReduce Cluster.
    Soila Kavulya, Jiaqi Tan, Rajeev Gandhi, Priya Narasimhan.
    In 10th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing (CCGrid) 2010, Melbourne, Victoria, Australia, May 2010. (Preprint)

  6. Kahuna: Problem Diagnosis for MapReduce-based Cloud Computing Environments.
    Jiaqi Tan, Xinghao Pan, Soila Kavulya, Eugene Marinelli, Rajeev Gandhi, Priya Narasimhan.
    In 12th IEEE/IFIP Network Operations and Management Symposium (NOMS) 2010, Osaka, Japan, Apr 2010. (Preprint)

  7. Blind Men and the Elephant: Piecing Together Hadoop for Diagnosis.
    Xinghao Pan, Jiaqi Tan, Soila Kavulya, Rajeev Gandhi, Priya Narasimhan.
    In 20th IEEE International Symposium on Software Reliability Engineering (ISSRE), Industrial Track, Mysuru, India, Nov 2009.

  8. Mochi: Visual Log-Analysis Based Tools for Debugging Hadoop.
    Jiaqi Tan, Xinghao Pan, Soila Kavulya, Rajeev Gandhi, Priya Narasimhan.
    In USENIX Workshop on Hot Topics in Cloud Computing (HotCloud '09), San Diego, CA, Jun 2009. (Paper)

  9. Ganesha: Black-Box Diagnosis for MapReduce Systems.
    Xinghao Pan, Soila Kavulya, Jiaqi Tan, Rajeev Gandhi, Priya Narasimhan.
    In Workshop on Hot Topics in Measurement & Modeling of Computer Systems (HotMetrics), Seattle, WA, Jun 2009. (Preprint)

  10. SALSA: Analyzing Logs as State Machines.
    Jiaqi Tan, Xinghao Pan, Soila Kavulya, Rajeev Gandhi, Priya Narasimhan.
    In USENIX Workshop on Analysis of System Logs (WASL), San Diego, CA, Dec 2008. (Preprint)

Failure Diagnosis for Distributed Systems

Publications

  1. Performance Troubleshooting in Data Centers: An Annotated Bibliography.
    Chengwei Wang, Soila Kavulya, Jiaqi Tan, Liting Hu, Mahendra Kutare, Michael Kasick, Karsten Schwan, Priya Narasimhan, Rajeev Gandhi.
    In ACM SIGOPS Operating Systems Review 47(3), November 2013. (Preprint)

  2. Transparent System Call Based Performance Debugging for Cloud Computing.
    Nikhil Khadke, Michael Kasick, Soila Kavulya, Jiaqi Tan, Priya Narasimhan.
    In USENIX Workshop on Managing Systems Automatically and Dynamically (MAD), Hollywood, CA, Oct 2012.

  3. Lightweight Black-box Failure Detection for Distributed Systems.
    Jiaqi Tan, Soila Kavulya, Rajeev Gandhi, Priya Narasimhan.
    In Workshop on Management of Big Data systems (MBDS) 2012, co-located with the International Conference on Autonomic Computing, San Jose, SA, Sep 2012.

  4. ASDF: An Automated, Online Framework for Diagnosing Performance Problems.
    Keith Bare, Soila Kavulya, Jiaqi Tan, Xinghao Pan, Eugene Marinelli, Michael Kasick, Rajeev Gandhi, Priya Narasimhan.
    Architecting Dependable Systems, in Lecture Notes in Computer Science, Volume 6420/2010, No. 7, Pages 201-226, 2010.

  5. Black Box Problem Diagnosis in Parallel File Systems.
    Michael Kasick, Jiaqi Tan, Rajeev Gandhi, Priya Narasimhan.
    In 8th USENIX Conference on File and Storage Technologies (FAST) 2010, San Jose, CA, Feb 2010.

  6. System-Call Based Problem Diagnosis for PVFS.
    Michael Kasick, Keith Bare, Eugene Marinelli, Jiaqi Tan, Rajeev Gandhi, Priya Narasimhan.
    In Workshop on Hot Topics in System Dependability (HotDep 2009), Estoril, Lisbon, Portugal, Jun 2009. (Preprint)

Other Activities

Publications

  1. Hadoop Framework: Impact of Data Organization on Performance.
    Yu Shyang Tan, Jiaqi Tan, Eng Siong Chng, Bu-Sung Lee, Jiaming Li, Susumu Date, Hui Ping Chak, Xiong Xiao, Atsushi Narishige.
    In Software: Practice and Experience, 43(11), John Wiley and Sons Ltd., May 2011.

  2. No More HotDependencies: Toward Dependency-Agnostic Upgrades in Distributed Systems.
    Tudor Dumitras, Jiaqi Tan, Zhengheng Gho, Priya Narasimhan.
    In Workshop on Hot Topics in System Dependability (HotDep), Edinburgh, Scotland, Jun 2007. (Preprint)

Academic Activities

  1. Shadow PC: ACM European Conference on Computer Systems (EuroSys) 2016

  2. External Reviewer: ACM User Interface Software and Technology Symposium (UIST) 2015

Teaching

  1. Teaching Assistant: 18-848D (Special Topics in Embedded Systems: Sports Technology), Spring 2015

  2. Teaching Assistant: 18-749 (Building Reliable Distributed Systems), Fall 2015

Contact Information

Email

tanjiaqi at cmu dot edu
jiaqi.tan at alumni dot cmu dot edu

Office

4720 Forbes Avenue, CIC 410
Pittsburgh, PA 15213, USA

Versions of papers provided on this page are meant only for personal or educational use, and are not intended for redistribution for any other purpose.