- 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
- 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
- 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
- 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]
- [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]
- [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]
- As Strong As Its Weakest Link: How to Break Blockchain DApps at RPC Service
- A Formal Analysis of the FIDO UAF Protocol
- [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]
- [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]
- 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
- 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
- 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
- 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
- 2019, IEEE S&P, Spectre attacks: Exploiting speculative execution
- 2018, USENIX Security, Meltdown: Reading Kernel Memory from User Space