@inproceedings{ifc-influence-ccs23, author = {McKenna McCall and Abhishek Bichhawat and Limin Jia}, title = {Tainted Secure Multi-Execution to Restrict Attacker Influence}, booktitle = {Proceedings of the 30th ACM Conference on Computer and Communications Security (CCS)}, year = {2023}, month = {to appear}, topic ={ifc,sec} } @inproceedings {ifttt-soups23, author = {McKenna McCall and Eric Zeng and Faysal Hossain Shezan and Mitchell Yang and Lujo Bauer and Abhishek Bichhawat and Camille Cobb and Limin Jia and Yuan Tian}, title = {Towards Usable Security Analysis Tools for {Trigger-Action} Programming}, booktitle = {Nineteenth Symposium on Usable Privacy and Security (SOUPS 2023)}, year = {2023}, isbn = {978-1-939133-36-6}, address = {Anaheim, CA}, pages = {301--320}, url = {https://www.usenix.org/conference/soups2023/presentation/mccall}, publisher = {USENIX Association}, month = aug, topic={ifttt,ifc,sec} } @INPROCEEDINGS {tee-csf23, author = {Farzaneh Derakhshan and Zichao Zhang and Amit Vasudevan and Limin Jia}, booktitle = {Proceedings of the IEEE 36th Computer Security Foundations Symposium (CSF)}, title = {Towards End-to-End Verified TEEs via Verified Interface Conformance and Certified Compilers}, year = {2023}, doi = {10.1109/CSF57540.2023.00021}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/tee-csf23.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/tee-csf23-tr.pdf}, month = jul, topic ={fm,sec} } @inproceedings{nodemedic-eurosp2023, title = {NodeMedic: End-to-End Analysis of Node.js Vulnerabilities with Provenance Graphs}, author = {Darion Cassel and Wai Tuck Wong and Limin Jia}, booktitle = {Proceedings of the IEEE European Symposium on Security and Privacy (Euro S&P)}, month = jul, year = 2023, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/nodemedic-eurosp23.pdf}, doi = {10.1109/EuroSP57164.2023.00068}, topic = {ifc,sec,js,fm}, } @article{intermittent-type-pldi2023, author = {Surbatovich, Milijana and Spargo, Naomi and Jia, Limin and Lucia, Brandon}, title = {A Type System for Safe Intermittent Computing}, year = {2023}, issue_date = {June 2023}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = {7}, number = {PLDI}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/curricle-pldi23.pdf}, doi = {10.1145/3591250}, journal = {Proc. ACM Program. Lang.}, month = jun, articleno = {136}, numpages = {25}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/curricle-tr.pdf}, topic ={pl,intermittent,ifc,rust} } @inproceedings{crash-type-esop23, author = {Derakhshan, Farzaneh and Dotzel, Myra and Surbatovich, Milijana and Jia, Limin}, title = {Modal Crash Types for Intermittent Computing}, year = {2023}, isbn = {978-3-031-30043-1}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/crash-type-esop23.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/crash-type-tr.pdf}, doi = {10.1007/978-3-031-30044-8_7}, booktitle = {Programming Languages and Systems: Proceedings of 32nd European Symposium on Programming (ESOP)}, pages = {168-196}, numpages = {29}, topic = {intermittent, pl}, } @inproceedings{compifc-eurosp2022, title = {IFC Compositional Information Flow Monitoring for Reactive Programs}, author = {McKenna McCall and Abhishek Bichhawat and Limin Jia}, shortauthor = {M. McCall and A. Bichhawat and L. Jia}, shortwhere = {Euro S&P'22}, booktitle = {Proceedings of the 2022 IEEE 7th European Symposium on Security and Privacy (Euro S&P)}, month = jun, year = 2022, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/compifc-eurosp22.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/compositional-ifc-tr.pdf}, doi = {10.1109/EuroSP53844.2022.00036}, topic = {ifc,sec}, } @inproceedings{evading-www2022, author = {Lin, Su-Chin and Chou, Kai-Hsiang and Chen, Yen and Hsiao, Hsu-Chun and Cassel, Darion and Bauer, Lujo and Jia, Limin}, title = {Investigating Advertisers' Domain-Changing Behaviors and Their Impacts on Ad-Blocker Filter Lists}, year = {2022}, isbn = {9781450390965}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/tracking-domains-www22.pdf}, doi = {10.1145/3485447.3512218}, booktitle = {Proceedings of the ACM Web Conference 2022 (WWW)}, pages = {576-587}, numpages = {12}, series = {WWW '22}, topic ={web,sec}, } @article{mobiletracking-pets2022, title = {{OmniCrawl}: Comprehensive Measurement of Web Tracking With Real Desktop and Mobile Browsers}, author = {Darion Cassel and Su-Chin Lin and Alessio Buraggina and William Wang and Andrew Zhang and Lujo Bauer and Hsu-Chun Hsiao and Limin Jia and Timothy Libert}, journal = {Proceedings on Privacy Enhancing Technologies (PETS)}, year = 2022, month = jan, volume = 2022, number = 1, doi = {10.2478/popets-2022-0012}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/omnicrawl-pets2022.pdf}, topic = {web,sec}, } @article{session-contract-journal22, title = {Session-typed concurrent contracts}, journal = {Journal of Logical and Algebraic Methods in Programming}, volume = {124}, pages = {100731}, year = {2022}, xissn = {2352-2208}, doi = {j.jlamp.2021.100731}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/session-journal22.pdf}, author = {Hannah Gommerstadt and Limin Jia and Frank Pfenning}, topic = {pl}, } @inproceedings{syrust-pldi21, author = {Takashima, Yoshiki and Martins, Ruben and Jia, Limin and P\u{a}s\u{a}reanu, Corina S.}, title = {{SyRust}: Automatic Testing of {Rust} Libraries with Semantic-Aware Program Synthesis}, year = {2021}, doi = {10.1145/3453483.3454084}, booktitle = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI)}, pages = {899-913}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/syrust-pldi21.pdf}, topic ={fm, rust}, } @inproceedings{ocelot-pldi21, author = {Surbatovich, Milijana and Jia, Limin and Lucia, Brandon}, title = {Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems}, year = {2021}, booktitle = {Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI)}, pages = {851-866}, doi = {10.1145/3453483.3454081}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/ocelot-pldi21.pdf}, topic = {intermittent,rust}, } @INPROCEEDINGS {gradual-csf21, author = {Abhishek Bichhawat and McKenna McCall and Limin Jia}, booktitle = {Proceedings of the IEEE 34th Computer Security Foundations Symposium (CSF)}, title = {Gradual Security Types and Gradual Guarantees}, month = jun, year = {2021}, pages={1-16}, doi = {10.1109/CSF51468.2021.00015}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/gradual-typing-csf21.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/gradual-typing-csf21-tr.pdf}, topic = {pl,ifc,sec}, } @INPROCEEDINGS{iosk-sp21, author={Yu, Miao and Gligor, Virgil and Jia, Limin}, booktitle={Proceedings of the 2021 IEEE Symposium on Security and Privacy (SP)}, title={An {I/O} Separation Model for Formal Verification of Kernel Implementations}, pages={572-589}, month = may, year={2021}, doi={10.1109/SP40001.2021.00101}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/iosk-sp21.pdf}, topic={fm,sec}, } @INPROCEEDINGS {node-permission:icse21, author = {Gabriel Ferreira and Limin Jia and Joshua Sunshine and Christian Kastner}, booktitle = {Proceedings of the 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)}, title = {Containing Malicious Package Updates in npm with a Lightweight Permission System}, month = {may}, year = {2021}, doi = {10.1109/ICSE43902.2021.00121}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/npm-permissions-icse21.pdf}, topic ={js,sec}, } @INPROCEEDINGS{session-ifc-lics21, author={Derakhshan, Farzaneh and Balzer, Stephanie and Jia, Limin}, booktitle={Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, title={Session Logical Relations for Noninterference}, year={2021}, doi={10.1109/LICS52264.2021.9470654}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/session-ifc-lics21.pdf}, topic={pl,ifc}, } @inproceedings{domxss-www21, author = {Melicher, William and Fung, Clement and Bauer, Lujo and Jia, Limin}, title = {Towards a Lightweight, Hybrid Approach for Detecting {DOM} {XSS} Vulnerabilities with Machine Learning}, booktitle = {Proceedings of the Web Conference (WWW)}, pages = {2684-2695}, year = {2021}, doi = {10.1145/3442381.3450062}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/www2021-dom-xss-dnn.pdf}, topic = {js,sec}, } @inproceedings{netter-vmcai21, author = {Han Zhang and Chi Zhang and Arthur Azevedo de Amorim and Yuvraj Agarwal and Matt Fredrikson and Limin Jia}, title = {{Netter}: Probabilistic, Stateful Network Models}, booktitle = {Proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)}, series = {Lecture Notes in Computer Science}, volume = {12597}, year = {2021}, doi = {10.1007/978-3-030-67067-2\_22}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/netter-vmcai21.pdf}, topic = {fm,network}, } @article{intermittent-foundation-oopsla20, author = {Surbatovich, Milijana and Lucia, Brandon and Jia, Limin}, title = {Towards a Formal Foundation of Intermittent Computing}, year = {2020}, issue_date = {November 2020}, volume = {4}, number = {OOPSLA}, doi = {10.1145/3428231}, journal = {Proc. ACM Program. Lang.}, month = nov, articleno = {163}, numpages = {31}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/intermittent-formal-oopsla20.pdf}, topic = {intermittent,fm}, } @inproceedings{netsmc-nsdi20, author ={Yifei Yuan and {Soo-Jin} Moon and Sahil Uppal and Limin Jia and Vyas Sekar}, title = {{NetSMC}: A Custom Symbolic Model Checker for Stateful Network Verification}, year = 2020, booktitle = {Proceedings of the 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI)}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/smc-nsdi20.pdf}, topic = {fm,network}, } @inproceedings{groundtruth-feast20, author = {Li, Kaiyuan and Woo, Maverick and Jia, Limin}, title = {On the Generation of Disassembly Ground Truth and the Evaluation of Disassemblers}, year = {2020}, pages = {9-14}, doi = {10.1145/3411502.3418429}, booktitle = {Proceedings of the 2020 ACM Workshop on Forming an Ecosystem Around Software Transformation}, series = {FEAST'20}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/ground-truth-feast20.pdf}, topic = {sec}, } @INPROCEEDINGS{compverify-fmcad20, author={Zhang, Zichao and de Amorim, Arthur Azevedo and Jia, Limin and Păsăreanu, Corina S.}, booktitle={Proceedings of the 2020 Formal Methods in Computer Aided Design (FMCAD)}, title={Automating Compositional Analysis of Authentication Protocols}, year={2020}, pages={113-118}, doi={10.34727/2020/isbn.978-3-85448-042-6_18}, url ={https://www.andrew.cmu.edu/user/liminjia/research/papers/taglierino-short-fmcad20.pdf}, topic = {fm,sec}, } @inproceedings{gradual-ifc-lics20, author = {de Amorim, Arthur Azevedo and Fredrikson, Matt and Jia, Limin}, title = {Reconciling Noninterference and Gradual Typing}, year = {2020}, booktitle = {Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, doi = {10.1145/3373718.3394778}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/glio-lics20.pdf}, topic = {ifc,pl}, } @inproceedings {ifttt-soups20, author = {Camille Cobb and Milijana Surbatovich and Anna Kawakami and Mahmood Sharif and Lujo Bauer and Anupam Das and Limin Jia}, title = {How Risky Are Real Users{\textquoteright} {IFTTT} Applets?}, booktitle = {Proceedings of the Sixteenth Symposium on Usable Privacy and Security ({SOUPS})}, year = {2020}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/ifttt-soups20.pdf}, topic ={ifttt,ifc,sec}, } @article{ibis-oopsla19, author = {Surbatovich, Milijana and Jia, Limin and Lucia, Brandon}, title = {{I/O} Dependent Idempotence Bugs in Intermittent Systems}, year = {2019}, issue_date = {October 2019}, volume = {3}, number = {OOPSLA}, doi = {10.1145/3360609}, journal = {Proc. ACM Program. Lang.}, month = oct, articleno = {183}, numpages = {31}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/ibis-oopsla19.pdf}, topic ={intermittent,fm}, } @inproceedings{flowpol-esorics19, author = {Darion Cassel and Yan Huang and Limin Jia}, title = {Uncovering Information Flow Policy Violations in {C} Programs (Extended Abstract)}, booktitle = {Proceedings of the 24th European Symposium on Research in Computer Security (ESORICS)}, year = 2019, doi = {10.1007/978-3-030-29962-0_2}, url ={https://www.andrew.cmu.edu/user/liminjia/research/papers/flownotation-esorics19.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/flownotation-tr.pdf}, topic ={ifc,sec}, } @inproceedings{ifc-csf18, author = {McKenna McCall and Hengruo Zhang and Limin Jia}, title = {Knowledge-based Security of Dynamic Secrets for Reactive Programs}, booktitle = {Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF)}, month = jul, year = 2018, doi={10.1109/CSF.2018.00020}, url ={https://www.andrew.cmu.edu/user/liminjia/research/papers/knowledge-csf18.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/sme-declassify-tr2018.pdf}, topic ={ifc,sec}, } @inproceedings{mikado-nsdi18, author = {Yifei Yuan and Sanjay Chandrasekaran and Limin Jia and Vyas Sekar}, title = {Efficient and Correct Test Scheduling for Ensembles of Stateful Network Policies}, booktitle = {Proceedings of the 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI)}, year = {2018}, url ={https://www.andrew.cmu.edu/user/liminjia/research/papers/scheduling-nsdi18.pdf}, topic ={network,fm}, } @inproceedings{session-esop18, author = {Hanna Gommerstadt and Limin Jia and F. Pfenning}, title = {Session-Typed Concurrent Contracts}, booktitle = {Proceedings of the 27th European Symposium on Programming (ESOP)}, month=apr, year = 2018, doi = {10.1007/978-3-319-89884-1_27}, url ={https://www.andrew.cmu.edu/user/liminjia/research/papers/contract-esop18.pdf}, topic ={pl}, } @inproceedings{domxss-ndss18, author = {William Melicher and Anupam Das and Mahmood Sharif and Lujo Bauer and Limin Jia}, title = {Riding out {DOM}sday: Toward detecting and preventing {DOM} cross-site scripting}, booktitle = {Proceedings of the 25th Network and Distributed System Security Symposium (NDSS)}, month = feb, year = 2018, doi = {10.1145/3442381.3450062}, url ={https://www.andrew.cmu.edu/user/liminjia/research/papers/ndss2018-taint-tracking.pdf}, topic ={js, web, sec,ifc}, } @article{provenance-18, author ={Ang Chen and Chen Chen and Lay Kuan Loh and Yang Wu and Andreas Haeberlen and Limin Jia and Boon Thau Loo and Wenchao Zhou}, title ={Data Center Diagnostics with Network Provenance}, year = 2018, volume = {41}, number = {1}, journal = {IEEE Data Eng. Bull.}, pages = {74-85}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/provenance-18.pdf}, topic ={network,fm}, } @inproceedings{ifttt-www17, author = {Milijana Surbatovich and Jassim Aljuraidan and Lujo Bauer and Anupam Das and Limin Jia}, title = {Some Recipes Can Do More Than Spoil Your Appetite: Analyzing the Security and Privacy Risks of {IFTTT} Recipes}, booktitle = {Proceedings of the 26th International World Wide Web Conference (WWW)}, month = apr, year = 2017, doi = {10.1145/3038912.3052709}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/ifttt-info-flows-www2017.pdf}, topic ={ifttt,sec,ifc}, } @inproceedings{dprov-sigmod17, author = {Chen Chen and Harshal Tushar Lehri and Lay Kuan Loh and Limin Jia and Boon Thau Loo and Wenchao Zhou}, title = {Distributed Provenance Compression}, booktitle = {Proceedings of the ACM SIGMOD/PODS}, month = may, year = 2017, doi = {10.1145/3035918.3035926}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/provenance-sigmod-tr.pdf}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/provenance-sigmod17.pdf}, topic = {network,fm}, } @inproceedings{counterfactual-plas17, author = {McKenna McCall and L. K. Loh and Limin Jia}, title = {A Sequent Calculus for Counterfactual Reasoning}, booktitle = {Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security (PLAS)}, year = 2017, doi = {10.1145/3139337.3139342}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/counterfactual-plas17.pdf}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/counterfactual-tr.pdf}, topic ={fm,ifc}, } @inproceedings{ifc-post17, author = {Willard Rafnsson and Limin Jia and Lujo Bauer}, title = {Timing-Sensitive Noninterference through Composition}, booktitle = {Proceedings of the 6th International Conference on Principles of Security and Trust (POST)}, month = apr, year = 2017, doi = {10.1007/978-3-662-54455-6_1}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/time-ni-post17.pdf}, topic ={ifc,sec}, } @inproceedings{uberspark-usenix16, author = {Amit Vasudevan and Sagar Chaki and Petros Maniatis and Limin Jia and Anupam Datta}, title = {\"{u}berSpark: Enforcing Verifiable Object Abstractions for automated Compositional Security Analysis of a Hypervisor }, booktitle = {Proceedings of the 25th USENIX Security}, month = aug, year = 2016, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/uberspark-sec16.pdf}, topic ={sec, fm}, } @inproceedings{msession-popl16, author = {Limin Jia and Hanna Gommerstadt and Frank Pfenning}, title = {Monitors and Blame Assignment for Higher-Order Session Types}, booktitle = {Proceedings of the 43rd ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)}, doi ={10.1145/2914770.2837662}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/session-blame-popl16.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/session-blame-tr2015.pdf}, year = {2016}, topic = {pl}, } @inproceedings{encryptedDB-ccs15, author = {Omar Chowdhury and Deepak Garg and Limin Jia and Anupam Datta}, title = {Equivalence-based Security for Querying Encrypted Databases: Theory and Application to Privacy Policy Audits}, booktitle = {Proceedings of the 22nd ACM Conference on Computer and Communications Security (CCS)}, year = 2015, doi = {10.1145/2810103.2813638}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/crypt-equiv-ccs2015.pdf}, topic = {sec,fm}, } @inproceedings{interface-csf15, author = {Limin Jia and Shayak Sen and Deepak Garg and Anupam Datta}, title = {A Logic of Programs with Interface-confined Code}, booktitle = {Proceedings of the 28th IEEE Computer Security Foundations Symposium (CSF)}, year = 2015, doi={10.1109/CSF.2015.38}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/systemM-csf2015.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/systemM-tr2015.pdf}, topic = {sec,pl,fm}, } @inproceedings{ifc-browser-ndss15, author = {Lujo Bauer and Shaoying Cai and Limin Jia and Tim Passaro and Michael Stroucken and Yuan Tian}, title = {Run-time monitoring and formal analysis of information flows in {Chromium}}, booktitle = {Proceedings of the 22nd Annual Network \& Distributed System Security Symposium (NDSS)}, year = 2015, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/chromium-taint-ndss2015.pdf}, topic = {ifc,sec}, } @inproceedings{ndlog-ppdp15, author = {Chen Chen and Lay Kuan Loh and Limin Jia and Wenchao Zhou and Boon T. Loo}, title = {Automated verification of safety properties of declarative networking programs}, booktitle = {Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming (PPDP)}, year = 2015, doi = {10.1145/2790449.2790516}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/ndlog-ver-ppdp2015.pdf}, topic = {network,fm}, } @inproceedings{android-soap14, author = {William Klieber and Lori Flynn and Amar Bhosale and Limin Jia and Lujo Bauer}, title = {{Android} Taint Flow Analysis for {App} Sets}, booktitle = {Proceedings of the 3rd ACM SIGPLAN International Workshop on the State of the Art in Java Program Analysis (SOAP)}, year = 2014, doi = {10.1145/2614628.2614633}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/ifc-android-soap14.pdf}, topic = {ifc, sec}, } @inproceedings{logging-trust14, author = {Arunesh Sinha and Limin Jia and Paul England and Jacob R. Lorch}, title = {Continuous Tamper-proof Logging Using {TPM} 2.0}, booktitle = {Proceedings of the 7th International Conference on Trust \& Trustworthy Computing (TRUST)}, year = 2014, doi = {10.1007/978-3-319-08593-7_2}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/securelogging-trust2014.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/securelogging-tr2014.pdf}, topic ={sec,fm}, } @inproceedings{ndlog-forte14, author = {Chen Chen and Limin Jia and Hao Xu and Cheng Luo and Wenchao Zhou and Boon T. Loo}, title = {A Program Logic for Verifying Secure Routing Protocols}, booktitle = {Proceedings of the IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE)}, year = 2014, doi ={10.1007/978-3-662-43613-4_8}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/sandlog-forte2014.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/sandlog-tr2014.pdf}, topic = {fm,network}, } @inproceedings{audit-codaspy14, author = {Oh, Se Eun and Chun, Ji Young and Jia, Limin and Garg, Deepak and Gunter, Carl A. and Datta, Anupam}, title = {Privacy-Preserving Audit for Broker-Based Health Information Exchange}, booktitle = {Proceedings of the ACM Conference on Data and Application Security and Privacy (CODASPY)}, year = 2014, doi = {10.1145/2557547.2557576}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/codaspy-2014.pdf}, topic = {sec,fm}, } @inproceedings{opt-ccs14, author = {Fuyuan Zhang and Limin Jia and Cristina Basescu and Tiffany Hyun-Jin Kim and Yih-Chun Hu and Adrian Perrig}, title = {Mechanized Network Origin and Path Authenticity Proofs}, booktitle = {Proceedings of the 21st ACM Conference on Computer and Communications Security (CCS)}, year = 2014, doi = {10.1145/2660267.2660349}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/opt-ccs2014.pdf}, topic = {network,sec,fm}, } @inproceedings{opt-sigcomm14, author = {Tiffany Hyun-Jin Kim and Limin Jia and Cristina Basescu and Soo Bum Lee and Yih-Chun Hu and Adrian Perrig}, title ={Lightweight Source Authentication and Path Validation}, booktitle = {Proceedings of the 2014 ACM Conference on Data Communication {SIGCOMM}}, year = 2014, doi = {10.1145/2740070.2626323}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/opt-sigcomm2014.pdf}, topic = {sec,network}, } @inproceedings{audit-cav14, author ={Omar Chowdhury and Limin Jia and Deepak Garg and Anupam Datta}, title = {Temporal Mode-Checking for Runtime Monitoring of Privacy Policies}, booktitle = {Proceedings of the 26th International Conference on Computer Aided Verification (CAV)}, year = 2014, doi = {10.1007/978-3-319-08867-9_9}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/precis-cav2014.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/precis-tr2014.pdf}, topic = {sec,fm}, } @inproceedings{xmhf-sp13, author ={Amit Vasudevan and Sagar Chaki and Limin Jia and Jon McCune and Jim Newsome and Anupam Datta}, title = {Design, Implementation and Verification of an e{X}tensible and Modular Hypervisor Framework}, booktitle = {Proceedings of the 2013 IEEE Symposium on Security and Privacy (SP)}, year = 2013, doi={10.1109/SP.2013.36}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/xmhf-oakland13.pdf}, topic = {sec,fm}, } @inproceedings{android-esorics13, author ={Limin Jia and Jassim Aljuraidan and Elli Fragkaki and Lujo Bauer and Michael Stroucken and Kazuhide Fukushima and Shinsaku Kiyomoto and Yutaka Miyake}, title = {Run-time enforcement of information-flow properties on Android (extended abstract)}, booktitle = {Proceedings of the 18th European Symposium on Research in Computer Security (ESORICS)}, year = 2013, doi = {10.1007/978-3-642-40203-6_43}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/android-esorics2013.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/android-pi-calculus-tr.pdf}, topic = {ifc,sec}, } @inproceedings{hippa-sacmat13, author = {Omar Chowdhury and Andreas Gampe and Jianwei Niu and Jeffery V. Ronne and Jared Bennatt and Anupam Datta and Limin Jia and William H. Winsborough}, title ={Privacy promises that can be kept: a policy analysis method with application to the {HIPAA} privacy rule}, booktitle = {Proceedings of the 18th ACM Symposium on Access Control and Technologies (SACMAT)}, year = 2013, doi = {10.1145/2462410.2462423}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/hippa-sacmat13.pdf}, topic = {sec,fm}, } @inproceedings{dlog-wripe12, author ={Chen Chen and Limin Jia and Boon Thau Loo and Wenchao Zhou}, title ={Reduction-based Security Analysis of Internet Routing Protocols}, booktitle = {2nd International Workshop on Rigorous Protocol Engineering (WRiPE)}, year = 2012, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/reduction-wripe12.pdf}, } @inproceedings{android-esorics12, author ={Elli Fragkaki and Lujo Bauer and Limin Jia and David Swasey}, title = {Modeling and Enhancing Android’s Permission System}, booktitle = {Proceedings of the 17th European Symposium on Research in Computer Security (ESORICS)}, year = 2012, doi = {10.1007/978-3-642-33167-1_1}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/android-esorics12.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/android-perm-tr.pdf}, topic = {ifc, sec}, } @article{dlog-comlan12, author = {Vivek Nigam and Limin Jia and Boon T. Loo and Andre Scedrov}, title = {Maintaining Distributed Logic Programs Incrementally}, journal = {Computer Languages, Systems \& Structures (COMLAN)}, volumn = {38}, issue = {2}, pages = {158-180}, publisher = {Elsevier Publishing}, year = 2012, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/ndlog-semantics-jrnl.pdf}, topic = {network,fm}, } @article{fsr-ton12, author = {Anduo Wang and Limin Jia and Wenchao Zhou and Yiqing Ren and Boon T. Loo and Jennifer Rexford and Vivek Nigam and Andre Scedrov and Carolyn Talcott}, title = {{FSR}: Formal Analysis and Implementation Toolkit for Safe Inter-domain Routing}, journal = {IEEE/ACM Transactions on Networking (ToN)}, volumn = {20}, issue = {6}, pages = {1814-1827}, year = 2012, doi = {10.1145/2043164.2018510}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/fsr_jrnl.pdf}, topic = {network, fm}, } @inproceedings{audit-ccs11, author = {Deepak Garg and Limin Jia and Anupam Datta}, title = {Policy Auditing over Incomplete Logs: Theory, Implementation and Applications}, booktitle = {Proceedings of the ACM Conference on Computer and Communications Security (CCS)}, month = oct, year = 2011, doi = {10.1145/2046707.2046726}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/audit-ccs11.pdf}, topic = {fm,sec}, } @inproceedings{comp-ICISS11, author ={Anupam Datta and Jeremy Blocki and Nicolas Christin and Henry DeYoung and Deepak Garg and Limin Jia and Dilsun Kaynar and Anuesh Sinha}, title ={Understanding and Protecting Privacy: Formal Semantics and Principled Audit Mechanisms}, booktitle = {Proceedings of the International Conference on Information Systems Security (ICISS)}, year = 2011, doi ={10.1007/978-3-642-25560-1_1}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/privacy-iciss11.pdf}, topic = {fm,sec}, } @inproceedings{ndlop-ppdp11, author ={Vivek Nigam and Limin Jia and Boon T. Loo and Andre Scedrov}, title ={Maintaining Distributed Logic Programs Incrementally}, booktitle = {Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP)}, month = jul, year = 2011, doi = {10.1145/2003476.2003495}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/incremental-ppdp.pdf}, topic = {fm,networks}, } @inproceedings{bgp-forte11, author ={Anduo Wang and Carolyn Talcott and Limin Jia and Boon T. Loo and Andre Scedrov}, title ={Analyzing {BGP} Instances in {Maude}}, booktitle = {Proceedings of the International Conference on Formal Techniques for Networked and Distributed Systems (FMOODS/FORTE)}, month = jun, year = 2011, doi = {10.1007/978-3-642-21461-5_22}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/maude-bgp.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/maude-bgp-tr.pdf}, topic = {networks,fm}, } @ARTICLE{comp-mag11, author={Datta, Anupam and Franklin, Jason and Garg, Deepak and Jia, Limin and Kaynar, Dilsun}, journal={IEEE Security Privacy}, title={On Adversary Models and Compositional Security}, year={2011}, volume={9}, number={3}, pages={26-32}, doi={10.1109/MSP.2010.203}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/sp2010-preprint.pdf}, topic = {fm,sec}, } @inproceedings{credential-csf10, author = {Lujo Bauer and Limin Jia and Divya Sharma}, title = {Constraining Credential Usage in Logic-based Access Control}, booktitle = {Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF)}, month = jul, year = 2010, doi={10.1109/CSF.2010.18}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/csf2010-constraints.pdf}, topic = {fm,sec}, } @inproceedings{hippa-wpes10, author ={Henry DeYoung and Deepak Garg and Limin Jia and Dilsun Kaynar and Anupam Datta}, title ={Experiences in the Logical Specification of the HIPAA and GLBA Privacy Laws}, booktitle = {Proceedings of the Workshop on Privacy in the Electronic Society (WPES)}, month = oct, year = 2010, doi = {10.1145/1866919.1866930}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/privacy-wpes.pdf}, topic = {fm,sec}, } @inproceedings{ndlog-lam10, author ={Vivek Nigam and Limin Jia and Boon T. Loo and Andre Scedrov}, title = {An Operational Semantics for Network {Datalog}}, booktitle = {3rd International Workshop on Logics, Agents Mobility (LAM '10)}, month = jul, year = 2010, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/psnCor-lam.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/ndlogsemans-tr.pdf}, topic = {network,fm}, } @inproceedings{dependent-popl10, author = {Limin Jia and Jianzhou Zhao and Vilhelm Sjöberg and Stephanie Weirich}, title = {Dependent Types and Program Equivalence}, booktitle = {Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL)}, month = jan, year = 2010, doi = {10.1145/1706299.1706333}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/popl10-lambda-eek.pdf}, topic = {pl}, } @inproceedings{fsr-hotnets09, author ={Anduo Wang and Limin Jia and Changbin Liu and Boon Thau Loo and Oleg Sokolsky and Prithwish Basu}, title = {Formally Verifiable Networking}, booktitle = {8th Workshop on Hot Topics in Networks (ACM SIGCOMM HotNets-VIII)}, month = oct, year = 2009, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/fvn-hotnets.pdf}, topic = {fm,network}, } @inproceedings{data-ppdp09, author = {Kenny Q. Zhu and Daniel S. Dantas and Kathleen Fisher and Limin Jia and Yitzhak Mandelbaum and Vivek Pai and David Walker}, title ={Language Support for Processing Distributed Ad Hoc Data}, booktitle = {Proceedings of the ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP)}, month = sep, year = 2009, doi = {10.1145/1599410.1599440}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/pads-ppdp.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research//pads-tr.pdf}, topic = {pl}, } @inproceedings{aura-plas09, author ={Limin Jia and Steve Zdancewic}, title = {Encoding Information Flow in {AURA}}, booktitle = {Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security (PLAS)}, month = jun, year = 2009, doi = {10.1145/1554339.1554344}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/aura-flow-plas.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research//aura-flow-tr.pdf}, topic = {sec,ifc}, } @inproceedings{xdomain-sacmat09, author = {Lujo Bauer and Limin Jia and Mike K. Reiter and David Swasey}, title ={{xDomain}: Cross-border Proofs of Access}, booktitle = {Proceedings of the 14th ACM Symposium on Access Control Models and Technologies (SACMAT)}, month = jun, year = 2009, doi = {10.1145/1542207.1542216}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/xdomain-sacmat.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/xdomain-tr.pdf}, topic = {sec,fm}, } @inproceedings{aura-icfp08, author = {Limin Jia and Jeffrey A. Vaughan and Karl Mazurak and Jianzhou Zhao and Luke Zarko and Joseph Schorr and Steve Zdancewic}, title = {{AURA}: A Programming Language for Authorization and Audit}, booktitle = {Proceedings of the 2008 SIGPLAN International Conference on Functional Programming (ICFP)}, month = sep, year = 2008, doi = {10.1145/1411203.1411212}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/aura-icfp.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/aura-tr.pdf}, topic = {pl,sec}, } @inproceedings{aura-csf08, author = {Jeffrey A. Vaughan and Limin Jia and Karl Mazurak and Steve Zdancewic}, title = {Evidence-based Audit}, booktitle = {Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF)}, month = jun, year = 2008, doi={10.1109/CSF.2008.24}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/aura-csf08.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/aura-audit-tr.pdf}, topic = {sec,fm}, } @misc{heap-shape-06, author = {Limin Jia and David Walker}, title = {Linear Logic, Heap-shape Patterns and Imperative Programming}, booktitle = {Princeton University Technical Report TR-762-06}, month = jul, year = 2006, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/shapes-TR.pdf}, topic = {fm}, } @inproceedings{heap-gpce06, author = {Fracis Perry and Limin Jia and David Walker}, title ={Expressing Heap-shape Contracts in Linear Logic}, booktitle = {Proceedings of the 5th International Conference on Generative Programming and Component Engineering (GPCE)}, month = oct, year = 2006, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/contract_gpce.pdf}, shorturl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/space06.pdf}, topic = {fm}, } @inproceedings{ilc-esop06, author = {Limin Jia and David Walker}, title ={ILC: A Foundation for Automated Reasoning About Pointer Programs}, booktitle = {Programming Languages and Systems: 15th European Symposium on Programming (ESOP), Lecture Notes in Computer Science 3924}, month = mar, year = 2006, doi = {10.1007/11693024_10}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/ilc_esop.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/ILC-TR-738.pdf}, topic = {fm}, } @inproceedings{tal-lics05, author = {Limin Jia and Francis Spalding and Neal Glew and David Walker}, title ={Certifying Compilation for a Language with Stack Allocation}, booktitle = {Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS)}, month = jun, year = 2005, doi = {10.1109/LICS.2005.9}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/stack-lics05.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/TR-724-05.pdf}, topic = {fm,pl}, } @inproceedings{modal-esop04, author ={Limin Jia and David Walker}, title = {Modal Proofs as Distributed Programs}, booktitle ={Programming Languages and Systems: 13th European Symposium on Programming (ESOP), Lecture Notes in Computer Science 2986}, doi = {10.1007/978-3-540-24725-8_16}, month = apr, year = 2004, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/esop04.pdf}, trurl = {https://www.andrew.cmu.edu/user/liminjia/research/papers/modal-proofs-as-programs-tr.pdf}, topic = {pl, fm}, } @inproceedings{storage-lics03, author ={Amal Ahmed and Limin Jia and David Walker}, title = {Reasoning About Hierarchical Storage}, booktitle = {Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS)}, month = jun, year = 2003, doi={10.1109/LICS.2003.1210043}, url = {https://www.andrew.cmu.edu/user/liminjia/research/papers/hierarchical-storage-lics03.pdf}, topic = {fm,pl}, }