About Me

I am a research engineer in the Information Division at DSO National Laboratories in Singapore. 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.

Previously, I completed my Ph.D. in Electrical and Computer Engineering at Carnegie Mellon University, under the supervision of Prof. Priya Narasimhan, where I was also affiliated with the Parallel Data Laboratory. (My previous webpage can be found here.) My Ph.D. thesis was "Prescriptive Safety-Checks through Automated Proofs for Control-Flow Integrity". Prior to that, 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.

Prescriptive Safety-Checks through Automated Proofs for Control-Flow Integrity

(Thesis Document)

Embedded software today is pervasive: they can be found everywhere, from coffee makers and medical devices, to cars and aircraft. Embedded software today is also open and connected to the Internet, exposing them to external attacks that can cause its Control-Flow Integrity (CFI) to be violated. Control-Flow Integrity is an important safety property of software, which ensures that the behavior of the software is not inadvertently changed. The violation of CFI in software can cause unintended behaviors, and can even lead to catastrophic incidents in safety-critical systems.

This dissertation develops a two-part approach for CFI: (i) prescribing source-code safetychecks, that prevent the root-causes of CFI, that programmers can insert themselves, and (ii) formally proving CFI for the machine-code of programs with source-code safety-checks. First, our prescribed safety-checks, when applied, prevent the root-causes of CFI, thereby enabling software to recover from CFI violations in a customizable way. In addition, our prescribed safety-checks are visible to programmers, empowering them to ensure that the behavior of their software is not inadvertently changed by the prescribed safety-checks. However, programmer-inserted safety-checks may be incomplete. Thus, current techniques for proving CFI, which assume that safety-checks are complete, may not work. Second, this dissertation develops a logic approach that automates formal proofs of CFI for the machine-code of software containing both source-code CFI safety-checks and system calls. We extend an existing trustworthy Hoare logic with new proof rules, proof tactics, and a novel proof-search algorithm, which exploit the principle of local reasoning for safety properties to automatically generate CFI proofs for the machine-code of programs compiled with our prescribed source-code safety-checks.

To the best of our knowledge, our approach to CFI is the first to combine programmer-visible source-code enforcement mechanisms for CFI–enabling programmers to customize them and observe that their software is not inadvertently changed–with machine-code proofs of CFI that can be automated, and that does not require a trusted or verified compiler to ensure its proven properties hold in machine-code. We evaluate our CFI approach on realistic embedded software. We evaluate our approach on the MiBench and WCET benchmarks, implementations of common file utilities, and programs interfacing with hardware inputs and outputs on the Raspberry Pi single-board-computer. The variety of our target programs, and our ability to support useful features such as file and hardware inputs and outputs, demonstrate the wide applicability of our approach.

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.
   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.
   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 with Errata) (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.

Mobile, Web, and IoT Security

Publications

1. A Survey of Security Vulnerabilities in Bluetooth Low Energy Beacons.
   Hui Jun Tay, Jiaqi Tan, and Priya Narasimhan.
   Carnegie Mellon University Parallel Data Laboratory Technical Report CMU-PDL-16-109, November 2016.

2. 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)

3. 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)

4. 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. Cachier: Edge-Caching for Recognition Applications. Utsav Drolia, Katherine Guo (Bell Labs, USA), Jiaqi Tan, Rajeev Gandhi, Priya Narasimhan. In IEEE 37th International Conference on Distributed Computing Systems (ICDCS), June 2017.

2. Towards edge-caching for image recognition. Utsav Drolia, Katherine Guo (Bell Labs, USA), Jiaqi Tan, Rajeev Gandhi, Priya Narasimhan. In 1st International Workshop on Smart Edge Computing and Networking (SmartEdge), co-located with the 15th IEEE International Conference on Pervasive Computing and Communications (PerCom), March 2017.

3. 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.

4. 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.

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. PC Member: Workshop on Middleware for Edge Clouds & Cloudlets (MECC) 2017 (co-located with ACM/IFIP/USENIX Middleware 2017 Conference)

2. PC Member: Workshop on Middleware for Edge Clouds & Cloudlets (MECC) 2016 (co-located with ACM/IFIP/USENIX Middleware 2016 Conference)

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

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

Teaching

1. Completed the Future Faculty Program at the Eberly Center for Teaching Excellence and Educational Innovation

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

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

Email

tjiaqi at dso dot org dot sg
jiaqit at alumni dot cmu dot edu

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.