Paper List

Usenix Security

2022

• Mining Node.js Vulnerabilities via Object Dependence Graph and Query
  • Node.js, Abstract Interpretation
• ProFactory: Improving IoT Security via Formalized Protocol Customization
  • IoT, Protocol
• SAPIC+: protocol verifiers of the world, unite!
  • Symbolic Security Protocol Verifier

2021

• MPInspector: A Systematic and Automatic Approach for Evaluating the Security of IoT Messaging Protocols
  • Formal Analysis(Tamarin Prover), IoT, Protocol
• Towards Formal Verification of State Continuity for Enclave Programs
  • Formal Analysis(Tamarin Prover), TEE
• DICE*: A Formally Verified Implementation of DICE Measured Boot
  • Formal Analysis, boot protocol
• EOSAFE: Security Analysis of EOSIO Smart Contracts
  • Symbolic Execution, EOSIO, Smart Contract
• EVMPatch: Timely and Automated Patching of Ethereum Smart Contracts
  • Smart Contract, Patch
• Evil Under the Sun: Understanding and Discovering Attacks on Ethereum Decentralized Applications
  • Dapp, DNN
• Smart Contract Vulnerabilities: Vulnerable Does Not Imply Exploited
  • Smart Contract
• SmarTest: Effectively Hunting Vulnerable Transaction Sequences in Smart Contracts through Language Model-Guided Symbolic Execution
  • Symbolic Execution, Smart Contract
• Frontrunner Jones and the Raiders of the Dark Forest: An Empirical Study of Frontrunning on the Ethereum Blockchain
  • smart contract
• Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor
  • Formally Verify(Coq), Hypervisor
• Automated Discovery of Denial-of-Service Vulnerabilities in Connected Vehicle Protocols
  • Model Checking(TLC), DoS
• Privacy-Preserving and Standard-Compatible AKA Protocol for 5G
  • Formal Analysis(Tamarin Prover), 5G

2020

• A Formal Analysis of IEEE 802.11's WPA2: Countering the Kracks Caused by Cracking the Counters
  • Formal Analysis(Tamarin Prover), Network, Protocol
• martVerif: Push the Limit of Automation Capability of Verifying Security Protocols by Dynamic Strategies
  • Formal Analysis(Tamarin Prover), Network, Protocol, Reinforcement Learning
• A Tale of Two Headers: A Formal Analysis of Inconsistent Click-Jacking Protection on the Web
  • Formal Analysis, Click-Jacking Protection
• APEX: A Verified Architecture for Proofs of Execution on Remote Devices under Full Software Compromise
  • Formal Analysis(VRASED), Embedded Devices
• The Ballot is Busted Before the Blockchain: A Security Analysis of Voatz, the First Internet Voting Application Used in U.S. Federal Elections
  • Voting, App
• VoteAgain: A scalable coercion-resistant voting system
  • Voting
• The Industrial Age of Hacking
  • Hacking
• A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols
  • Formal Analysis(Tamarin Prover), Diffie-Hellman Protocols
• TXSPECTOR: Uncovering Attacks in Ethereum from Transactions
  • Smart Contract, Transactions

IEEE S&P

2022

• SAILFISH: Vetting Smart Contract State-Inconsistency Bugs in Seconds
• [Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documents]
• [Four Attacks and a Proof for Telegram]
• [A Formal Security Analysis of the W3C Web Payment APIs: Attacks and Verification]
• [Cats vs. Spectre: An Axiomatic Approach to Modeling Speculative Execution Attacks]
• [TASHAROK: Using Mechanism Design for Enhancing Security Resource Allocation in Interdependent Systems]
• [Formal Model-Driven Discovery of Bluetooth Protocol Design Vulnerabilities]

2021

• [SmartPulse: Automated Checking of Temporal Properties in Smart Contracts]
• [An Interactive Prover for Protocol Verification in the Computational Model]
• [An I/O Separation Model for Formal Verification of Kernel Implementations]
• [Symbolic Modeling of Micro Services for Intrusion Detection]
• [A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer]
• [Bookworm Game: Automatic Discovery of LTE Vulnerabilities Through Documentation Analysis]
• [SGUARD: Towards Fixing Vulnerable Smart Contracts Automatically]
• [Compositional Security for Reentrant Applications]

2020

• [Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level]
• [VerX: Safety Verification of Smart Contracts]
• [VeriSmart: A Highly Precise Safety Verifier for Ethereum Smart Contracts]
• [Semantic Understanding of Smart Contracts: Executable Operational Semantics of Solidity]

NDSS

2021

• As Strong As Its Weakest Link: How to Break Blockchain DApps at RPC Service
• A Formal Analysis of the FIDO UAF Protocol

2020

• SODA: A Generic Online Detection Framework for Smart Contracts

CCS

2022

• [Cerberus: A Formal Approach to Secure and Efficient Enclave Memory Sharing]
• [Zapper: Smart Contracts with Data and Identity Privacy]
• [VRust: Automated Vulnerability Detection for Solana Smart Contracts]
• [Understanding Security Issues in the NFT Ecosystem]
• [Towards Automated Safety Vetting of Smart Contracts in Decentralized Applications]
• [Towards Automated Safety Vetting of Smart Contracts in Decentralized Applications]

2020

• [ACE: Asynchronous and Concurrent Execution of Complex Smart Contracts]
• [eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts]
• [WI is Almost Enough: Contingent Payment All Over Again]
• [BlackMirror: Preventing Wallhacks in 3D Online FPS Games]
• [Forensic Analysis in Access Control: Foundations and a Case-Study from Practice]

Binary Similarity

• 2019, NDSS, Neural machine translation inspired binary code similarity comparison beyond function pairs
• 2019, IEEE S&P, Asm2vec: Boosting static representation robustness for binary clone search against code obfuscation and compiler optimization
• 2018, USENIX Security, Precise and Accurate Patch Presence Test for Binaries
• 2017, ACM SIGSAC, Neural network-based graph embedding for cross-platform binary code similarity detection
• 2016, ACM SIGSAC, Scalable graph-based bug search for firmware images
• 2014, ACM SIGSOFT, Semantics-based obfuscation-resilient binary code similarity comparison with applications to software plagiarism detection

Vulnerabilities Detection

• 2019, USENIX Security, Looking from the Mirror: Evaluating IoT Device Security through Mobile Companion Apps
• 2019, IEEE, ProFuzzer: On-the-fly Input Type Probing for Better Zero-Day Vulnerability Discovery
• 2019, IEEE, Razzer: Finding kernel race bugs through fuzzing
• 2018, Science and Information Conference, Survey of automated vulnerability detection and exploit generation techniques in cyber reasoning systems
• 2018, USENIX Security, Precise and accurate patch presence test for binaries
• 2018, ACM SIGPLAN, FirmUp- Precise Static Detection of Common Vulnerabilities in Firmware
• 2018, ACM SIGSAC, Using logic programming to recover C++ classes and methods from compiled executables
• 2018, NDSS, VulDeePecker: A deep learning-based system for vulnerability detection
• 2016, ACM on Asia Conference on Computer and Communications Security, Automated dynamic firmware analysis at scale: a case study on embedded web interfaces
• 2016, NDSS, Towards Automated Dynamic Analysis for Linux-based Embedded Firmware
• 2014, NDSS, AVATAR: A Framework to Support Dynamic Security Analysis of Embedded Systems' Firmwares
• 2014, USENIX Security, A Large-Scale Analysis of the Security of Embedded Firmwares
• 2013, USENIX Security, {FIE} on Firmware: Finding Vulnerabilities in Embedded Systems Using Symbolic Execution

Fuzz

• 2019, USENIX Security, FIRM-AFL: High-Throughput Greybox Fuzzing of IoT Firmware via Augmented Process Emulation
• 2019, NDSS, REDQUEEN: Fuzzing with Input-to-State Correspondence
• 2019, NDSS, PeriScope: An Effective Probing and Fuzzing Framework for the Hardware-OS Boundary
• 2018, IEEE SP, T-Fuzz: fuzzing by program transformation
• 2018, IEEE SP, Angora: Efficient fuzzing by principled search
• 2018, IEEE SP, CollAFL: Path sensitive fuzzing
• 2018, ACM SIGSAC, Evaluating Fuzz Testing
• 2018, ACM SIGSAC, Hawkeye: towards a desired directed grey-box fuzzer
• 2018, NDSS, Iotfuzzer: Discovering memory corruptions in iot through app-based fuzzing
• 2018, NDSS, What You Corrupt Is Not What You Crash: Challenges in Fuzzing Embedded Devices
• 2017, USENIX ATC, CAB-Fuzz: Practical Concolic Testing Techniques for {COTS} Operating Systems

Smart Contracts

• 2019, NDSS, Sereum- Protecting Existing Smart Contracts Against ReEntrancy Attacks
• 2018, USENIX Security, Erays: reverse engineering ethereum's opaque smart contracts
• 2018, ACM SIGSAC, BitML: a calculus for Bitcoin smart contracts
• 2018, ACM SIGSAC, Securify: Practical security analysis of smart contracts

Natural Language Processing

• 2017, EMNLP, Deal or no deal? end-to-end learning for negotiation dialogues

Operating System Security

• 2019, IEEE S&P, Spectre attacks: Exploiting speculative execution
• 2018, USENIX Security, Meltdown: Reading Kernel Memory from User Space