Limin Jia's Publications

OmniCrawl: Comprehensive measurement of Web tracking with real desktop and mobile browsers.
Darion Cassel, Su-Chin Lin, Alessio Buraggina, William Wang, Andrew Zhang, Lujo Bauer, Hsu-Chin Hsiao, Limin Jia, and Timothy Libert. In PETS 2022, to appear.

Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems.
Milijana Surbatovich, Limin Jia, and Brandon Lucia.
In Proceedings of the ACM Programming Language Design and Implementation (PLDI), June 2021. [PDF]

SyRust: Automatic Testing of Rust Libraries with Semantic-Aware Program Synthesis.
Yoshiki Takashima, Ruben Martins, Limin Jia, and Corina S Pǎsǎreanu.
In Proceedings of the ACM Programming Language Design and Implementation (PLDI), June 2021. [PDF]

Gradual Security Types and Gradual Guarantees.
Abhishek Bichhawat, McKenna McCall, and Limin Jia.
In Proceedings of the 34th IEEE Computer Security Foundations Symposium (CSF), June 2021. [PDF] An earlier TR appeared as arXiv:2003.12819

An I/O Separation Model for Formal Verification of Kernel Implementations.
Miao Yu, Virgil Gligor, and Limin Jia.
In Proceedings of IEEE Symposium on Security & Privacy, May 2021. [PDF]

Containing Malicious Package Updates in npm with a Lightweight Permission System.
Gabriel Ferreira, Limin Jia, Joshua Sunshine, and Christian Kastner.
In Proceedings of the IEEE/ACM 43rd International Conference on Software Engineering (ICSE), May 2021. [PDF]

Towards a lightweight, hybrid approach for detecting DOM XSS vulnerabilities with machine learning.
William Melicher, Clement Fung, Lujo Bauer, and Limin Jia.
In Proceedings of the 30th The Web Conference (TheWebConf'21), April 2021. [PDF]

Netter: Probabilistic, Stateful Network Models.
A Han Zhang, Chi Zhang, Arthur Azevedo de Amorim, Yuvraj Agarwal, Matt Fredrikson, and Limin Jia.
In Proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2021. [PDF]

Towards a Formal Foundation of Intermittent Computing.
Milijana Surbatovich, Brandon Lucia, and Limin Jia.
In Proceedings of ACM on Programming Languages, Issue OOPSLA, November 2020. [PDF] Long version appeared as arXiv:2007.15126

On the Generation of Disassembly Ground Truth and the Evaluation of Disassemblers.
Kaiyuan Li, Maverick Woo, and Limin Jia
In Proceedings of the 2020 ACM Workshop on Forming an Ecosystem Around Software Transformation, November 2020. [PDF] Long version appeared as arXiv:2012.09155

Automating Compositional Analysis of Authentication Protocols.
Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia and Corina Pasareanu.
In Proceedings of Formal Methods in Computer-Aided Design (FMCAD), September 2020. [PDF]

How risky are real users' IFTTT applets?
Camille Cobb, Milijana Surbatovich, Anna Kawakami, Mahmood Sharif, Lujo Bauer, Anupam Das, and Limin Jia
In Proceedings of the 16th Symposium on Usable Privacy and Security (SOUPS), August 2020. [PDF]

Reconciling noninterference and gradual typing.
Arthur Azevedo de Amorim, Matt Fredrikson, and Limin Jia.
In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), July 2020. [PDF]

NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification.
Yifei Yuan, Soo-jin Moon, Sahil Uppal, Limin Jia, and Vyas Sekar.
In Proceedings of the 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI), April 2020. [PDF]

I/O Dependent Idempotence Bugs in Intermittent Systems.
Milijana Surbatovich, Limin Jia, and Brandon Lucia.
In Proceedings of ACM on Programming Languages, Volume 3, Issue OOPSLA , October 2019. [PDF]

Uncovering Information Flow Policy Violations in C Programs (Extended Abstract).
Darion Cassel, Yan. Huang, and Limin Jia.
In Proceedings of the 24th European Symposium on Research in Computer Security (ESORICS) , September 2019. Long version appeared as arXiv:1907.01727

Knowledge-based Security of Dynamic Secrets for Reactive Programs.
McKenna McCall, Hengruo Zhang, and Limin Jia.
In Proceedings of 31st IEEE Computer Security Foundations Symposium (CSF), to appear 2018.
Long version appeared as Carnegie Mellon University Technical Report CMU-CyLab-18-001, 2018. [PDF]

Session-Typed Concurrent Contracts.
Hannah Gommerstadt, Limin Jia, and Frank Pfenning.
In Proceedings of the 27th European Symposium on Programming (ESOP), April 2018. [PDF]

Efficient and Correct Test Scheduling for Ensembles of Stateful Network Policies.
Yifei Yuan, Sanjay Chandrasekaran, Limin Jia, and Vyas Sekar.
In Proceedings of the 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI), April 2018. [PDF]

Riding out DOMsday: Toward detecting and preventing DOM cross-site scripting.
William Melicher, Anupam Das, Mahmood Sharif, Lujo Bauer, and Limin Jia.
In Proceedings of the 25th Network and Distributed System Security Symposium (NDSS), February 2018. [PDF]

Data Center Diagnostics with Network Provenance.
Ang Chen, Chen Chen, Lay Kuan Loh, Yang Wu, Andreas Haeberlen, Limin Jia, Boon Thau Loo, and Wenchao Zhou.
In IEEE Data Eng. Bull. 41(1): 74-85 2018. [PDF]

A Sequent Calculus for Counterfactual Reasoning.
McKenna McCall, LayKuan Loh, and Limin Jia.
In Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security (PLAS), October 2017. [PDF]
Long version appeared as Carnegie Mellon University Technical Report CMU-CyLab-17-003, 2017. [PDF]

Distributed Provenance Compression.
Chen Chen, Harshal Tushar Lehri, Lay Kuan Loh, Limin Jia, Boon Loo and Wenchao Zhou.
In Proceedings of ACM SIGMOD/PODS, May 2017. [PDF]
Long version appeared as Carnegie Mellon University Technical Report CMU-CyLab-17-001, 2017. [PDF]

Timing-Sensitive Noninterference through Composition.
Willard Rafnsson, Limin Jia and Lujo Bauer.
In Proceedings of 6th International Conference on Principles of Security and Trust (POST), April 2017. [PDF]

Some Recipes Can Do More Than Spoil Your Appetite: Analyzing the Security and Privacy Risks of IFTTT Recipes.
Milijana Surbatovich, Jassim Aljuraidan, Lujo Bauer, Anupam Das and Limin Jia.
In Proceedings of 26th International World Wide Web Conference (WWW), April 2017. [PDF]

überSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor.
Amit Vasudevan and Sagar Chaki and Petros Maniatis and Limin Jia and Anupam Datta.
In Proceedings of 25th USENIX Security Symposium (USENIX Security 16), Aug. 2016. [PDF]

Monitors and Blame Assignment for Higher-Order Session Types.
Limin Jia, Hannah Gommerstadt, and Frank Pfenning.
In Proceedings of 43rd ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL) , Jan. 2016. [PDF]
Long version appeared as Carnegie Mellon University Technical Report CMU-CyLab-15-004, 2015. [PDF]

Equivalence-based Security for Querying Encrypted Databases: Theory and Application to Privacy Policy Audits.
Omar Chowdhury, Deepak Garg, Limin Jia, and Anupam Datta.
In Proceedings of ACM Conference on Computer and Communications Security (CCS) , Nov. 2015. [PDF]

A Logic of Programs with Interface-confined Code.
Limin Jia, Shayak Sen, Deepak Garg, and Anupam Datta.
In Proceedings of 28th IEEE Computer Security Foundations Symposium (CSF), July 2015. [PDF]
Long version appeared as Carnegie Mellon University Technical Report CMU-CyLab-13-001, 2013 (updated 2015). [PDF]

Automated Verification of Safety Properties of Declarative Networking Programs.
Chen Chen, Lay Kuan Loh, Limin Jia, Wenchao Zhou, and Boon Thau Loo.
In Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming (PPDP), July 2015. [PDF]

Run-time monitoring and formal analysis of information flows in Chromium.
Lujo Bauer, Shaoying Cai, Limin Jia, Tim Passaro, Michael Strouchen, and Yuan Tian.
In Proceedings of the 22nd Annual Network & Distributed System Security Symposium (NDSS), February 2015. [PDF]

Mechanized Network Origin and Path Authenticity Proofs.
Fuyuan Zhang, Limin Jia, Cristina Basescu, Tiffany Hyun­Jin Kim, Yih­Chun Hu, and Adrian Perrig.
In 21st ACM Conference on Computer and Communications Security (CCS), November 2014. [PDF]

Lightweight Source Authentication and Path Validation.
Tiffany Hyun-Jin Kim, Limin Jia, Cristina Basescu, Soo Bum Lee, Yih-Chun Hu, and Adrian Perrig.
In ACM SIGCOMM, August 2014. [PDF]

Temporal Mode-Checking for Runtime Monitoring of Privacy Policies.
Omar Chowdhury, Limin Jia, Deepak Garg, and Anupam Datta.
In 26th International Conference on Computer Aided Verification (CAV), July 2014. [PDF]
Long version appeared as Carnegie Mellon University Technical Report CMU-CyLab-14-005, May 2014. [PDF]

Continuous Tamper-proof Logging Using TPM 2.0.
Arunesh Sinha, Limin Jia, Paul England, and Jacob R. Lorch
In 7th International Conference on Trust & Trustworthy Computing (TRUST), June 2014. [PDF]
Long version appeared as Carnegie Mellon University Technical Report CMU-CyLab-13-008, July 2013. [PDF]

A Program Logic for Verifying Secure Routing Protocols.
Chen Chen, Limin Jia, Hao Xu, Cheng Luo, Wenchao Zhou, and Boon Thau Loo.
In IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE), June 2014. [PDF]
Long version appeared as University of Pennsylvania Technical Report, Feb. 2014. [PDF]

Privacy-Preserving Audit for Broker-Based Health Information Exchange.
Se Eun Oh, Ji Young Chun, Limin Jia, Deepak Garg, Carl A. Gunter, and Anupam Datta.
In ACM Conference on Data and Application Security and Privacy (CODASPY), Feb. 2014. [PDF]

Run-time enforcement of information-flow properties on Android (extended abstract).
Limin Jia, Jassim Aljuraidan, Elli Fragkaki, Lujo Bauer, Michael Stroucken, Kazuhide Fukushima, Shinsaku Kiyomoto, and Yutaka Miyake.
In Computer Security -- ESORICS 2013: 18th European Symposium on Research in Computer Security, Sept. 2013. [PDF]
Technical Report [PDF]

A Formal Framework for Secure Routing Protocols.
Chen Chen, Limin Jia, Hao Xu, Cheng Luo, Wenchao Zhou, and Boon Thau Loo
In Workshop on Foundations of Computer Security, June 2013. [PDF]

Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework.
Amit Vasudevan, Sagar Chaki, Limin Jia, Jonathan McCune, James Newsome, and Anupam Datta.
In IEEE Symposium on Security & Privacy, May 2013. [PDF]

Modeling and enhancing Android's permission system.
Elli Fragkaki, Lujo Bauer, Limin Jia, and David Swasey.
In Computer Security -- ESORICS 2012: 17th European Symposium on Research in Computer Security, Sept. 2012. [PDF]
Technical Report [PDF]

Maintaining Distributed Logic Programs Incrementally.
Vivek Nigam, Limin Jia, Boon Thau Loo and Andre Scedrov.
In Computer Languages, Systems & Structures (COMLAN), Elsevier Publishing, 2012. [PDF]

FSR: Formal Analysis and Implementation Toolkit for Safe Inter-domain Routing.
Anduo Wang, Limin Jia, Wenchao Zhou, Yiqing Ren, Boon Thau Loo, Jennifer Rexford, Vivek Nigam, Andre Scedrov and Carolyn L. Talcott.
In IEEE/ACM Transactions on Networking (ToN), 2012. [PDF]

Policy Auditing over Incomplete Logs: Theory, Implementation and Applications.
Deepak Garg, Limin Jia and Anupam Datta
In ACM Conference on Computer and Communications Security (CCS 2011), Oct 2011. [PDF]

On Adversary Models and Compositional Security.
Anupam Datta, Jason Franklin, Deepak Garg, Limin Jia and Dilsun Kaynar.
IEEE Security and Privacy Magazine, special issue on the Science of Security, 2011. [PDF]

FSR: Formal Analysis and Implementation Toolkit for Safe Inter-domain Routing.
Yiqing Ren, Wenchao Zhou, Anduo Wang, Limin Jia, Alexander J.T. Gurney, Boon Thau Loo and Jennifer Rexford.
ACM SIGCOMM Conference on Data Communication (demonstration), Aug 2011.

Maintaining Distributed Logic Programs Incrementally.
Vivek Nigam, Limin Jia, Boon Thau Loo and Andre Scedrov.
In 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP), July 2011. [PDF]

Analyzing BGP Instances in Maude.
Anduo Wang, Carolyn L. Talcott, Limin Jia, Boon Thau Loo and Andre Scedrov.
In International Conference on Formal Techniques for Networked and Distributed Systems (FMOODS/FORTE), June 2011. [PDF]
Technical Report [PDF]

Experiences in the Logical Specification of the HIPAA and GLBA Privacy Laws.
Henry DeYoung, Deepak Garg, Limin Jia, Dilsun Kaynar and Anupam Datta.
In WPES 2010: Workshop on Privacy in the Electronic Society, October 2010. [PDF]

Constraining Credential Usage in Logic-based Access Control.
Lujo Bauer, Limin Jia and Divya Sharma.
In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF), July 2010. [PDF]

An operational semantics for Network Datalog.
Vivek Nigam, Limin Jia, Anduo Wang, Boon T. Loo and Andre Scedrov.
In 3rd International Workshop on Logics, Agents, and Mobility (LAM '10), July 2010. [PDF]
Long version: [PDF]

Dependent Types and Program Equivalence.
Limin Jia, Jianzhou Zhao, Vilhelm Sjoberg and Stephanie Weirich.
In Proceedings of 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), January 2010. [PDF]

Formally Verifiable Networking.
Anduo Wang, Limin Jia, Changbin Liu, Boon Thau Loo, Oleg Sokolsky and Prithwish Basu.
In 8th Workshop on Hot Topics in Networks (ACM SIGCOMM HotNets-VIII), October 2009. [PDF]

Language Support for Processing Distributed Ad Hoc Data.
Kenny Q. Zhu, Daniel S. Dantas, Kathleen Fisher, Limin Jia, Yitzhak Mandelbaum, Vivek Pai and David Walker.
In Proceedings of ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP), September 2009. [PDF]
Long version appeared as Princeton Univ. Technical Report TR-826-08, July 2008. [PDF]

Encoding Information Flow in AURA.
Limin Jia and Steve Zdancewic.
In Proceedings of ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security (PLAS 2009), June 2009. [PDF]
Long version appeared as Univ. of Pennsylvania Technical Report MS-CIS-09-08, July 2008. [PDF]

xDomain: Cross-border proofs of access.
Lujo Bauer, Limin Jia, Michael K. Reiter, and David Swasey.
In Proceedings of the 14th ACM Symposium on Access Control Models and Technologies, June 2009. [PDF]
Long version appeared as Carnegie Mellon University Technical Report CMU-CyLab-09-005. [PDF]

AURA: A programming language for authorization and audit.
Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr and Steve Zdancewic.
In Proceedings of the 2008 SIGPLAN International Conference on Functional Programming (ICFP), September 2008. [PDF]
Long version appeared as Univ. of Pennsylvania Technical Report MS-CIS-08-10, July 2008. [PDF]

Evidence-based Audit.
Jeffrey A. Vaughan, Limin Jia, Karl Mazurak and Steve Zdancewic.
In Proceedings of 21st IEEE Computer Security Foundations Symposium (CSF), June 2008. [PDF]
Long version appeared as Univ. of Pennsylvania Technical Report MS-CIS-08-09, April 2008. [PDF]

Linear Logic, Heap-shape Patterns and Imperative Programming.
Limin Jia and David Walker. [PDF]
Long version appeared as Princeton University Technical Report TR-762-06, July 2006. [PDF]

Expressing Heap-shape Contracts in Linear Logic.
Frances Perry, Limin Jia and David Walker.
In Proceedings of the 5th International Conference on Generative Programming and Component Engineering (GPCE), October 2006. [PDF]
An earlier version appeared in the Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE), January 2006. [PDF]

ILC: A Foundation for Automated Reasoning About Pointer Programs.
Limin Jia and David Walker.
In Programming Languages and Systems: 15th European Symposium on Programming, ESOP 2006, Lecture Notes in Computer Science 3924, March 2006. [PDF]
Super short version appeared in 20th IEEE Symposium on Logic in Computer Science (LICS), short paper, June 2005. [PDF]
Long version appeared as Princeton University Technical Report TR-738-05, October 2005. [PDF]

Certifying Compilation for a Language with Stack Allocation.
Limin Jia, Frances Spalding, David Walker and Neal Glew.
In Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS), June 2005. [PDF]
Long version appeared as Princeton University Technical Report TR-724-05, March 2005. [PDF]

Modal Proofs as Distributed Programs (extended abstract).
Limin Jia and David Walker.
In Programming Languages and Systems: 13th European Symposium on Programming, ESOP 2004, Lecture Notes in Computer Science 2986, April 2004. [PDF]
Long version appeared as Princeton University Technical Report TR-671-03, August 2003. [PDF]

Reasoning About Hierarchical Storage.
Amal Ahmed, Limin Jia and David Walker.
In Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS), June 2003. [PDF]

Linear Logic and Imperative Programming.
Limin Jia. PhD thesis.
Computer Science Department, Princeton University, January 2008. [PDF]