Loading...

Quality Assurance Platform For Smart Contracts

Smart contracts that can falsify functional properties (correctness and security properties)

Smart contracts that can verify functional properties (correctness and security properties)

Smart contracts that can optimize the performance

Three Core Techniques

is an advanced technique for conducting deep analysis of the behavior of a program to determine what inputs cause each part of the program to execute.
By assuming symbolic values for inputs rather than obtaining concrete values as normal execution of a smart contract would, the symbolic execution engine in FractalTrust has the capability to systematically explore the program behavior and uncover corner cases.
Specifically, it leverages customized symbolic execution algorithms to enumerate path that are critical to the validity of functional and performance properties, including those due to fallback functions.
It is able to rank the criticalness of the paths and check the feasibility of paths that are likely to have security vulnerabilities. It also prioritizes the exploration by giving preference to paths that involve monetary transactions.
Thus with limited computing resources FractalTrust follows the money, which is often sufficient in capturing vulnerabilities in smart contracts.
is an algorithmic technique for proving that a property holds on a model of a software system under all possible execution conditions. It is one of the mainstream verification techniques for the design of computer hardware and other safety-critical systems, where bug fixing after product deployment is practically impossible and recall leads to huge financial loss.
The main advantage of model checking, compared to fuzz testing and symbolic execution, is the ability to verify properties. That is, when a functional or performance property holds in a smart contract, it may be able to generate a mathematical proof.
The model checking engine in FractalTrust consists of three innovative components: a model builder to capture the precise semantics of a smart contract, a framework to specify a wide range of functional and performance properties, and a set of algorithms to efficiently verify the property in the model, e.g., using fully automated abstraction and refinement techniques.
is an automated software testing  technique used to discover coding errors and security loopholes.
The fuzz testing engine in FractalTrust offers a high benefit-to-cost ratio and can reveal many serious defects overlooked by smart contract developers. It accomplishes this by generating a massive amount of input data (called seeds) for the test subject. It also leverages advanced static analysis and constraint-solving techniques to drastically improve the quality of the seeds.
First, static program analysis is used to identify critical, financial transaction related paths in a smart contract.
Then, the path is analyzed using constraint solvers to produce seeds that help explore the path during concrete execution.
FractalTrust also leverages the unique characteristics of properties and sensitive paths to increase the effectiveness of seeds. It can detect not only functional bugs regarding the correctness and security of smart contracts, but also performance bugs that lead to gas waste or DoS attacks.
Their synergistic and complementary strengths may be understood as follows. Fuzz testing is a computationally efficient technique for detecting bugs in smart contract quickly, whereas symbolic execution is a more comprehensive and systematic technique for exploring program paths and uncover the subtle bugs.
In both cases, the explored behavior constitutes a sound under-approximation of the actual behavior. Model checking, on the other hand, focuses on a sound over-approximation of the behavior of a smart contract.
Therefore, inside FractalTrust, model checking is geared toward verifying functional and performance properties, whereas fuzz testing and symbolic execution are geared toward detecting violations.

Core Team Members

Meghna

James Yang

Lab Director, PhD, University of Pennsylvania

James is a Professor of Computer Science at Western Michigan University.  He is an author of more than 80 scientific papers and an inventor of 10 United States patents. He received many awards, including 2018 ACM SIGSOFT Distinguished Paper Award, and 2008 ACM TODAES Best Journal Paper of the Year award. He was a visiting professor at the University of Michigan and an intern at Bell Labs. He also served as a panelist for the U.S. National Science Foundation, the NASA PostDoc Grant, and the U.S. Department of Energy Startup Fund. He is the general chair of the 12th IEEE Conference on Software Testing, Validation and Verification. 

Meghna

Jun Sun

Lab vice-director, PhD and PostDoc, National University of Singapore

Jun is currently an Associate Professor of Computer Science at Singapore University of Technology and Design. He was a visiting scholar at MIT. He was a recipient of the 2018 ACM SIGSOFT Distinguished Paper Award and the 2017 ACM SIGSOFT Distinguished Paper Award. He is the co-founder of the PAT model checker, which has been commercialized and used by dozens of companies including JAXA (a.k.a. Japanese NASA). He has published more than 180 journal and conference papers including top conferences in multiple areas.

Meghna

Chao Wang

Lab vice-director, PhD, University of Colorado at Boulder

Chao is an Associate Professor of Computer Science at University of Southern California. He was a faculty member at Virginia Tech, and a research staff member at NEC Laboratories of America, Inc. He has published more than 70 papers and received many awards, including the 2013 FMCAD Best Paper award and the 2010 ACM SIGSOFT Distinguished Paper award.

Meghna

Yu Jiang

Scientist, PhD, Tsinghua University, PostDoc,  University of Illinois at Urbana-Champaign

Yu is an Assistant Professor at Tsinghua University. He has published more than 50 papers in international journals and conferences. He was the recipient of the 2015 Chinese Computer Association Outstanding Doctoral Dissertation award, and the 2017 Excellent Guide Teacher Award for national software test competition.

Meghna

Rui Wang

Scientist, PhD, Tsinghua University

Rui is an Associate Professor of Information Engineering at Capital Normal University, China, where she is currently an Associate Professor. Her research interests include formal verification and their applications in blockchain ecosystems.

Cooperant Media