ASE 2019 (series) / Demonstrations /
Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts
Wed 13 Nov 2019 10:00 - 10:40 at Kensington Ballroom - Poster Session: Tool Demonstrations 2
Thu 14 Nov 2019 15:00 - 15:10 at Cortez 1 - Program Analysis Chair(s): Coen De Roover
Thu 14 Nov 2019 15:00 - 15:10 at Cortez 1 - Program Analysis Chair(s): Coen De Roover
An effective way to maximize code coverage in software tests is through dynamic symbolic execution, a technique that uses constraint solving to systematically explore a program’s state space. We introduce an open-source dynamic symbolic execution framework called Manticore for analyzing binaries and Ethereum smart contracts. Manticore’s flexible architecture allows it to support both traditional and exotic execution environments, and its API allows users to customize their analysis. Here, we discuss Manticore’s architecture and demonstrate the capabilities we have used to find bugs and verify the correctness of code for our commercial clients.
Wed 13 Nov Times are displayed in time zone: Tijuana, Baja California change
Wed 13 Nov
Times are displayed in time zone: Tijuana, Baja California change
| 10:00 - 10:40 Demonstration | TsmartGP: A Tool for Finding Memory Defects with Pointer Analysis Demonstrations Yuexing WangTsinghua University, Guang ChenTsinghua University, Min ZhouTsinghua University, Ming GuTsinghua University, Jiaguang SunTsinghua University | ||
| 10:00 - 10:40 Demonstration | BuRRiTo: A Framework to Extract, Specify, Verify and Analyze Business Rules Demonstrations Pavan ChittimalliTCS Research, Kritika AnandTCS Research, Shrishti PradhanTCS Research, Sayandeep MitraTCS Research, Chandan PrakashTCS Research, Rohit ShereTCS Research, Ravindra NaikTCS Research, TRDDC, India | ||
| 10:00 - 10:40 Demonstration | Lancer: Your Code Tell Me What You Need Demonstrations Shufan ZhouSchool of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Beijun ShenSchool of Electronic Information and Electrical Engineering, Shanghai Jiao Tong University, Hao ZhongShanghai Jiao Tong University | ||
| 10:00 - 10:40 Demonstration | TestCov: Robust Test-Suite Execution and Coverage Measurement Demonstrations Pre-print Media Attached File Attached | ||
| 10:00 - 10:40 Demonstration | Prema: A Tool for Precise Requirements Editing, Modeling and Analysis Demonstrations Yihao HuangEast China Normal University, Jincao FengEast China Normal University, Hanyue ZhengEast China Normal University, Jiayi ZhuEast China Normal University, Shang WangEast China Normal University, Siyuan JiangEastern Michigan University, Weikai MiaoShanghai Key Lab for Trustworthy Computing, School of Computer Science and Software Engineering, East China Normal University, Geguang PuEast China Normal University&Shanghai Trusted Industrial Control Platform Co., Ltd | ||
| 10:00 - 10:40 Demonstration | XRaSE: Towards Virtually Tangible Software using Augmented Reality Demonstrations Rohit MehraAccenture Labs, India, Vibhu Saujanya SharmaAccenture Labs, Vikrant KaulgudAccenture Labs, India, Sanjay PodderAccenture | ||
| 10:00 - 10:40 Demonstration | MuSC: A Tool for Mutation Testing of Ethereum Smart Contract Demonstrations Zixin LiNanjing University, Haoran WuState Key Laboratory for Novel Software Technology, Nanjing University, Jiehui XuNanjing University, Xingya WangState Key Laboratory for Novel Software Technology, Nanjing University, Lingming ZhangThe University of Texas at Dallas, Zhenyu ChenNanjing University | ||
| 10:00 - 10:40 Demonstration | VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-Threaded Programs with Lazy-CSeq Demonstrations Bernd FischerStellenbosch University, Salvatore La TorreUniversità degli Studi di Salerno, Gennaro ParlatoUniversity of Molise | ||
| 10:00 - 10:40 Demonstration | DeepMutation++: a Mutation Testing Framework for Deep Learning Systems Demonstrations Qiang HuKyushu University, Japan, Lei MaKyushu University, Xiaofei XieNanyang Technological University, Bing YuKyushu University, Japan, Yang LiuNanyang Technological University, Singapore, Jianjun ZhaoKyushu University | ||
| 10:00 - 10:40 Demonstration | Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts Demonstrations Mark MossbergTrail of Bits, Felipe ManzanoTrail of Bits, Eric HennenfentTrail of Bits, Alex GroceTrail of Bits, Gustavo GriecoTrail of Bits, Josselin FeistTrail of Bits, Trent BrunsonTrail of Bits, Artem DinaburgTrail of Bits Media Attached | ||
| 10:00 - 10:40 Demonstration | ConVul: An Effective Tool for Detecting Concurrency Vulnerabilities Demonstrations Ruijie MengUniversity of Chinese Academy of Sciences, Biyun ZhuUniversity of Chinese Academy of Sciences, Hao YunUniversity of Chinese Academy of Sciences, Haicheng LiUniversity of Chinese Academy of Sciences, Yan CaiInstitute of Software, Chinese Academy of Sciences, Zijiang YangWestern Michigan University | ||
| 10:00 - 10:40 Demonstration | mCUTE: A Model-level Concolic Unit Testing Engine for UML State Machines Demonstrations Reza AhmadiQueen's University, Karim JahedQueen's University, Juergen DingelQueen's University, Kingston, Ontario | ||
Thu 14 Nov Times are displayed in time zone: Tijuana, Baja California change
Thu 14 Nov
Times are displayed in time zone: Tijuana, Baja California change
13:40 - 15:20: Program AnalysisPapers / Research Papers / Demonstrations at Cortez 1 Chair(s): Coen De RooverVrije Universiteit Brussel | |||
| 13:40 - 14:00 Talk | Debreach: Mitigating Compression Side Channels via Static Analysis and Transformation Research Papers Brandon PaulsenUniversity of Southern California, Chungha SungUniversity of Southern California, Peter PetersonUniversity of Minnesota Duluth, Chao WangUSC | ||
| 14:00 - 14:20 Talk | Fine-grain memory object representation in symbolic execution Research Papers Martin NowackImperial College London | ||
| 14:20 - 14:40 Talk | RENN: Efficient Reverse Execution with Neural-Network-assisted Alias Analysis Research Papers Dongliang MuNanjing University, Wenbo GuoThe Pennsylvania State University, Alejandro CuevasThe Pennsylvania State University, Yueqi ChenThe Pennsylvania State University, Jinxuan GaiThe Pennsylvania State University, Xinyu XingThe Pennsylvania State University, Bing MaoNanjing University, Chengyu SongUC Riverside | ||
| 14:40 - 15:00 Talk | Batch Alias Analysis Research Papers Pre-print | ||
| 15:00 - 15:10 Demonstration | Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts Demonstrations Mark MossbergTrail of Bits, Felipe ManzanoTrail of Bits, Eric HennenfentTrail of Bits, Alex GroceTrail of Bits, Gustavo GriecoTrail of Bits, Josselin FeistTrail of Bits, Trent BrunsonTrail of Bits, Artem DinaburgTrail of Bits Media Attached | ||
| 15:10 - 15:20 Demonstration | BuRRiTo: A Framework to Extract, Specify, Verify and Analyze Business Rules Demonstrations Pavan ChittimalliTCS Research, Kritika AnandTCS Research, Shrishti PradhanTCS Research, Sayandeep MitraTCS Research, Chandan PrakashTCS Research, Rohit ShereTCS Research, Ravindra NaikTCS Research, TRDDC, India | ||