Hachi
We do security research on Cardano
Enter Hachi
Hachi is a research effort in security, programming language theory, and formal methods on the Cardano blockchain. More specifically, we study Cardano smart contract security and build software solutions to support this goal.
As a new platform for dApp, Cardano is exciting to both builders and users who invest much effort and capital. However, there are very few blockchains with scripting support for UTXO-based ledgers and even fewer built on functional programming and lambda calculus. The lack of tooling in these early days motivates us to work to improve the safety of the ecosystem.
Hachi aims to define more security standards on Cardano. We will open-source most of our work to the whole community.
The Work
Hachi’s work is highly experimental, diverse, and moves fast as we are still in the early days of smart contracts on the Cardano platform.
The main effort of the initial phase is on the low-level representations of validator scripts, starting from their on-chain serialized form of Plutus Core (PLC). This choice offers good precision as we work directly with what is deployed to the blockchain. Our tools will, by default, guarantee compatibility with different source languages of validators, be it Plutus or anything else.
At the time of writing, our focus is on the dynamic analysis of PLC, which consists of new frameworks for symbolic execution, concolic execution, instrumentation, fuzzers, and more. Our goal is to find input data triggering security issues on validators in single- or multi-transaction contexts.
In addition, we have experimented with static analysis and look forward to going deeper into the direction of semantic analysis, targeting both high- and low-level code.
Furthermore, we have been putting much effort into improving Cardano documentation and helping to find and fix bugs in their blockchain core. We also study common vulnerabilities in smart contract designs to raise security awareness among developers.
Other lines of work include solutions to monitor real-time attacks, patching and migrating deployed validator scripts once severe bugs are discovered, and more. Our backlog also covers future technologies like KEVM, IELE, and even other blockchains, smart contract architectures, and programming languages.
For now, we prioritize experimenting, building tools, contributing to the Cardano ecosystem, and publishing technical blogs. We plan to release research papers, attend conferences, and have more activities to keep connecting with the community in the long run.
Roadmap
Good work takes time. While we intend to bring proper tooling to the Cardano ecosystem as quickly as possible, we expect more progressive output to ensure that the result is mature enough for the public.
For Q4 2021, we look forward to releasing our first toolset, including a Hachi index to synchronize data from the blockchain, a PLC to Racket transpiler, and a suite of Racket engines for symbolic execution concolic execution, instrumentation, and fuzzers on the transpiled code.
In the future, our ambitious goal is to expand Hachi to a broader platform to support more programming languages, smart contract architectures, runtime, and blockchains. We aim to build an open playground for blockchain security researchers and engineers worldwide, with the Hachi DAO expected to be launched in August 2022.
Hachi Team
Hai Nguyen Quang.
@kk-hainq
Hai Nguyen Quang is a software engineer involved in several Cardano projects in MELD, ADAmatic, Indigo, and more. These ambitious endeavors have built a deep paranoia for security research in him. Despite not being specialized in the relevant fields, Hai is willing to do anything to push Hachi forward.
Quang Luong.
@quangio
Quang Luong is a formidable security engineer possessing a comprehensive skillset around SecOps & smart contract security. Besides penetration testing and reverse engineering, he has experience in high-performance systems, network protocols, and cryptography.
Quang has been leading several projects in Hachi, including a PLC to Racket transpiler and a symbolic execution engine in Racket.
Nguyen Anh Quynh.
@aquynh
Dr. Nguyen Anh Quynh is a regular speaker at cybersecurity conferences such as Blackhat, Defcon, Recon, and many more. He also presented his research in academic venues such as Usenix, IEEE, ACM, LNCS. His contributions to the field (like his reversing trilogy in Capstone, Unicorn, and Keystone) lay the foundation for various innovative works in the cybersecurity industry and academia. Dr. Nguyen’s code entered many modern systems such as web browsers, Android, Linux kernel, and more. Some of his security toolsets have been downloaded multiple million times.
Dr. Nguyen was the co-founder and Head of Lab at Verichains, where he co-authored several security research papers and talks on Ethereum smart contract security. He built Monocerus — the dynamic analysis framework for Ethereum and the first-ever grey box fuzzer for EVM bytecode.
Dr. Nguyen has been leading the development of instrumentation and fuzzers for PLC.
Nicolas Jeannerod.
@Niols
Dr. Nicolas Jeannerod is a Tweag computer scientist who enjoys specifications, abstraction, and modularization. He firmly believes in strongly typed functional programming, compilers, formal methods, and program verification.
He did his Ph.D. at Université de Paris on applying formal techniques to Shell scripts to find bugs in Debian packages. This venture led him to do both theoretical and practical research to build a concrete, efficient tool at the end. This research was published and discussed in various conferences, including technical conferences such as the Debian Conference. He then left academia, went to Tweag I/O, and joined Hachi to satisfy his need for concrete and industrial impact research.
Nicolas has been working on a concolic execution engine for PLC and exploring more ideas in Hachi in general.
Michael B. Gale.
@mbg
Michael B. Gale is a Tweag software engineer specializing in designing and implementing programming languages, development tools, and automation.
He worked as a Senior Teaching Fellow at the University of Warwick during 2017-2021, where he taught modules on Functional Programming in Haskell and Cyber Security. He taught functional programming to close to one thousand students during that time, extensively using property-based testing and emphasizing the benefits of reusable and strongly typed code.
At Hachi, Michael has been working on tooling and exploring new target representations to transpile PLC.
Partners
MELD has helped found, operate, and fund Hachi entirely up till now. MELD needs dedicated security research in Hachi to achieve its DeFi ambition on the blockchain. Security is the number one focus to providing efficient financial instruments to the mass.
MELD engineers offer help when relevant work is needed. We thank those who already contributed, including Duc, Khanh, Thanh, and a few interns.
Tweag is an important figure in the project’s development, with several people working with the Hachi team.
Trivia
Hachi is the number 8 in Japanese (八), which stays the same when we mirror it vertically or horizontally. It emphasizes the importance of both low-level and high-level representations and the consistency of the compilation pipeline in between.
Hachi also means bees in Japanese (蜂), which portrays hard-working creatures who attack and defend fiercely for their home.