Please describe your proposed solution

We propose to expand and open-source the XSY property-based testing toolkit and bundle it into a no-code command line tool. The XSY smart contract testing toolkit is already capable of identifying a large number of common smart contract vulnerabilities, including the dust token attack and the large datum attack.

There are a number of property-based testing frameworks that were designed specifically for use with Cardano smart contracts. However, they never really see much adoption. This is because utilizing these tools requires a significant investment and development effort that production DApps simply cannot afford to spend. Indeed, they must prioritize feature development to stay competitive. Our product is an out-of-the-box general-purpose testing tool along with a command-line interface that requires no time investment and can be applied by any DApp to identify common vulnerabilities via the use of property-based tests.

Including the following common vulnerabilities:

• Dust Token Attack
• Large Datum Attack
• Double Satisfaction
• Staking Control Theft
• Authentication Token Smuggling
• Validity Range Attack
• Signature Reuse Attack
• Liquidity and Assets Stealing Attack

The framework for this toolkit was developed specifically for a live mainnet protocol. The strength of this tool is partly due to a number of methodologies that we have employed specifically for testing and verifying smart contracts, such as the test objectives (i.e., translating parts of the specification into concrete, testable assertions) and attacks (i.e., automatically attempting a large set of predefined transaction modifications during testing to assess the robustness of validators).

The XSY automated penetration testing toolkit will be extended with the aim of achieving the following goals:

• Accessibility: The tool will be designed to be as easy to use as possible. The tool will be able to run attacks on any Cardano smart contract with absolutely minimal effort from the contract developers.

• Generalized: The tool will work with any type of smart contract (DApp, Lending, Marketplace, etc) without any specialization. This means the tool will be universally useful to every DApp on Cardano.

• Extensibility: Out of the box the tool is capable of identifying most common smart contract vulnerabilities. However, advanced users will also have the possibility to create and publish more general (or specialized) attacks. The tool will be designed to facilitate external contributions.

• Documentation: To encourage adoption the tool will be extensively documented with tutorials, guidelines for contributions, and practical usage examples showcasing how to run the tool on any smart contract.

Please define the positive impact your project will have on the wider Cardano community

The enhanced safety of Cardano’s smart contract platform is frequently advertised. This has been further supported by the absence of any large scale DeFi hacks of Plutus smart contracts. However, as the DeFi ecosystem continues to grow so too will be the number of bad actors attempting to exploit DApps. Currently, DApps are not taking advantage of many of the security mechanisms and strengths provided by the functional design of the Cardano smart contract system because the time investment required to do so is significant. Furthermore, the costs of an audit can be prohibitive to many protocols and even when it isn’t, often projects will opt to direct those funds towards feature development instead. This tool can significantly reduce the engineering hours required to conduct a thorough audit. The tool takes care of identifying all the common vulnerabilities that auditors would otherwise have to attempt to find in meticulous manual review. This allows auditors to focus on ensuring the correctness of the business logic and architecture of the protocol.

The XSY testing command-line tool automatically identifies common smart contract vulnerabilities via our pre-made general purpose property-based smart contract attack framework. This requires no development effort on behalf of the user. It is language agnostic and can be applied to any smart contract (Aiken, PlutusTx, Plutarch, Plu-Ts) with little to no development effort.

In addition to the utility provided by the penetration testing command-line tool, the property-based testing framework itself can be a powerful tool for DApp developers in Cardano. For instance, debugging on Cardano has been notoriously difficult due to obscure error reporting mechanisms. This tool can help developers identify the root-cause of an error by providing a detailed description of the transaction which triggered it.

What is your capability to deliver your project with high levels of trust and accountability? How do you intend to validate if your approach is feasible?

We know that the tool itself is effective. The tool already exists in a non-generalized form and is used in production. It identified a number of critical issues in a production high-complexity codebase.

What are the key milestones you need to achieve in order to complete your project successfully?

Milestone 1: Release DApp specific penetration testing framework for Cardano smart contracts. This includes open sourcing the existing testing framework for conducting attacks on Cardano smart contracts. This includes a set of predefined general attacks that can be applied to any contract. This milestone is the framework, not the command-line tool. The framework is well documented and designed to be easy to use; however, property-based testing can be quite involved, and it can be tough for developers who are unfamiliar with similar tooling to utilize it in practice.

Milestone Outputs:

• Open-sourced existing testing framework for conducting attacks on Cardano smart contracts.
• Predefined set of general attacks that can be applied to any contract.
• Comprehensive documentation for using the framework.

Acceptance Criteria:

• Approval of the testing framework and predefined attacks by the project lead.
• Approval of documentation by the project lead.

Evidence of Milestone Completion:

• Submission of the testing framework code to GitHub repository.
• Submission of predefined general attacks documentation.
• Submission of comprehensive framework documentation.

Milestone 2: Research on generalization and reducing development effort required to utilize the tool. This will focus on research and specification of the command-line smart contract penetration testing tool. We will provide thorough documentation for the command-line tool as-well-as the framework at-large. This documentation will serve as a step-by-step guide for developers to leverage the power of this tool to run penetration tests on any Cardano smart contract.

Milestone Outputs:

• Research report and specification for the command-line smart contract penetration testing tool.
• Thorough documentation for the command-line tool and the framework at large.

Acceptance Criteria:

• Approval of research report and specifications by the project lead.
• Approval of command-line tool documentation by the project lead.

Evidence of Milestone Completion:

• Submission of research report and specifications.
• Submission of command-line tool documentation to GitHub repository.

Milestone 3: Extend the framework with new general attack types to cover more common smart contract vulnerabilities. This will involve aggregating a list of common vulnerabilities that the tool does not currently account for and then introducing new attack types to the tool to make sure they are covered.

Milestone Outputs:

• Aggregated list of common vulnerabilities not currently covered.
• New attack types added to the tool to cover these vulnerabilities.

Acceptance Criteria:

• Approval of the list of new vulnerabilities and attack types by the project lead.
• Successful integration of new attack types into the framework.

Evidence of Milestone Completion:

• Submission of the list of new vulnerabilities.
• Submission of code and documentation for new attack types to GitHub repository.

Milestone 4: Introduce functionality to the tool to automatically query for a comprehensive set of "happy case" transactions for any given smart contract. The common vulnerabilities are described in the form of attacks in the toolkit. Attacks are mutations that can be applied to transactions to attempt to perform actions that should not be allowed. If a happy-case transaction still succeeds after applying an attack, then the tool flags it as a potential vulnerability and outputs that information to the developer along with information on potential resolutions. In order to effectively conduct this penetration testing on a smart contract protocol a large number of happy-case transactions are needed to cover each possible action that a protocol can support. Currently, transactions are either required to be built within the tool, or serialized transactions are to be loaded into the framework in order to facilitate attack mutations.

By introducing this query functionality, the user simply needs to provide the script hash of the contract(s) they want to test, and the tool will automatically query the given network to find a comprehensive set of happy-case transactions to apply the attacks to. This way it doesn't matter what offchain framework the protocol is built with; the tool will be able to conduct the attacks on any Cardano protocol irrespective of the protocol's tech stack.

Milestone Outputs:

• Functionality to automatically query a comprehensive set of "happy case" transactions for any given smart contract.
• Detailed documentation and user guide for using the new query functionality.

Acceptance Criteria:

• Successful implementation and testing of the query functionality.
• Approval of documentation and user guide by the project lead.

Evidence of Milestone Completion:

• Submission of query functionality code to GitHub repository.
• Submission of detailed documentation and user guide.

Milestone 5: Command-line tool publication

This includes the full release of the command-line tool which can be used to perform automated penetration testing on any Cardano smart contract protocol. The command-line tool will be intuitive and simple, allowing immediate use without any prior training or learning curve.

Milestone Outputs:

• Full release of the command-line tool for automated penetration testing on any Cardano smart contract protocol.
• Comprehensive documentation and user manual for the command-line tool.

Acceptance Criteria:

• Successful deployment and testing of the command-line tool.
• Approval of the command-line tool and documentation by the project lead.

Evidence of Milestone Completion:

• Release of command-line tool code and documentation on GitHub repository.
• Demonstration of the tool performing a live penetration test.

Final Milestone: Project Close-out Report and Video

A report detailing KPIs and how they were addressed along with the future roadmap for the XSY smart contract penetration testing toolkit.

A video that goes over the development process of the tool and demonstrates the tool performing a live penetration test of a smart contract protocol.

Who is in the project team and what are their roles?

Jean-Frédéric Etienne has more than 15 years of experience in safety and threat analysis and is an expert in several formal verification techniques. He is currently the architecture and technical lead for the Djed implementation on Cardano and has put in place a property-based testing methodology to extensively assess the correctness and robustness of Plutus smart contracts against all potential attacks. He has also specified and proved the adaptation of the Djed protocol on the EUTxO model and has developed a set of Plutus libraries to produce optimized on-chain code.

Jann Müller is a Haskell programmer with years of experience in writing scalable, mission-critical systems. He has been working with Plutus since its inception and is the maintainer of the sc-tools library for Cardano apps. He is the lead developer of XSY and will be working on the off-chain parts of the framework.

Philip DiSarro is an expert in the field of Compiler Development & Programming Language Theory. He has made significant open-source contributions to the Cardano developer ecosystem. As a co-chair of the IOHK developer experience working group he worked to identify and resolve pain points that DApp developers experience in Cardano. He has a vast wealth of professional experience in smart contract security and auditing on Cardano; and was responsible for the identification and resolution of a large number of critical exploits in production open-source smart contracts. Recently, Philip has concentrated his efforts on designing and deploying effective zero-knowledge proof applications within the Cardano ecosystem. Philip is a senior Haskell developer on the XSY team, a consultant and lecturer for Emurgo, and the CEO and co-founder of Anastasia Labs.

Amir H. Meyssami Rad is a Haskell developer and a member of the XSY development team with over two years of experience in developing on Cardano. His expertise spans wallet integration tools, off-chain transaction library development, DApp and on-chain development using Plutus across various projects.

Konstantinos Lambrou-Latreille is a Haskell programmer with more than 5 years of relevant experience. He worked for 3 years in IOG on Plutus off-chain tooling such as a node emulator for testing Plutus applications, a transaction building library, and a chain-indexer.

Please provide a cost breakdown of the proposed work and resources

1 X Haskell Engineer

1 X Haskell Test/QA Engineer

1 X Technical Writer

Some of this work will be done in parallel.

2 x Engineer

• Expanding attacks
• ~36 weeks
• ~140k Ada each

1 x Engineer

• Command-line design
• ~20 weeks
• ~80k Ada

1 x Engineer

• Command-line implementation
• ~24 weeks
• ~90k Ada

1 x Engineer

• Documentation
• ~12 weeks
• ~48k Ada

No dependencies.

How does the cost of the project represent value for money for the Cardano ecosystem?

The cost of the project represents significant value for money for the Cardano ecosystem by enhancing security through an automated toolkit that identifies common vulnerabilities, thereby safeguarding investments and maintaining trust. This allows DApp developers to focus on feature development, thanks to the toolkit's ease of use and minimal required effort, which accelerates innovation and deployment. The toolkit's language-agnostic nature and applicability to all types of smart contracts ensures universal accessibility, benefiting a wide range of projects. Automating vulnerability detection reduces the costs associated with manual audits, particularly benefiting smaller projects or startups. In fact, for many low-complexity DApps, this tool has the potential to eliminate the need for expensive audits. Moreover, the tool should generally reduce the cost of smart contract audits on Cardano. Currently, a significant portion of the time and effort in an audit is dedicated to manually scanning the entire codebase for common vulnerabilities. This tool automates that work, allowing auditors to focus on auditing the business logic or more application-specific aspects of the protocol. This significantly reduces the time required to perform a comprehensive audit, which should, in turn, lower the prices of audits, making them more accessible and affordable for the entire ecosystem. Furthermore, the open-source nature and extensibility of the toolkit encourage community contributions and collaboration, fostering a culture of security and transparency. Extensive documentation and tutorials further raise awareness about security best practices and empower developers to build more secure applications from the outset. This investment provides the Cardano ecosystem with a powerful tool that not only enhances security but also supports the growth and development of its diverse DApps and smart contracts.