Algorand Foundation Grant Application

[ehildenb]

https://algorandfoundation.submittable.com/submit/58a1352f-414b-4ed3-8ef1-193f1b9db97e/algorand-foundation-request-for-funding

[geo2a]

K Framework semantics of TEAL

Project Goal and Motivation

Goals

This project intends to build:

• a formal, executable and open-source semantics of TEAL available to everyone;
• through the Haskell backend of K, a formal verification tool for TEAL programs;
• through the LLVM backend of K, a simulation and unit-testing framework with the performance comparable to the reference implementation.

Non-goals

We do not intend to build a replacement of the existing Algorand node implementation, therefore the model does not encompass the block consensus and validation rewards.

Motivation

The Algorand DeFi ecosystem is experiencing a boom of new projects that utilise the platform's scalability and fast transaction finality. The developer community is vibrant, productive and supportive, as witnessed by the active developer-focused Discourd community with nearly two thousand active members and many active discussions on Twitter. We also see a major surge of requests for security audits of Algorand smart contracts. In response to that surge, the Algorand auditors team at RV has grown significantly over the past months. While the auditing services we provide for Algroand at the moment mostly comprise manual code review and pen-and-paper reasoning, we already have two clients (name them here?) requesting full mechanised formal verification of their smart contracts.

At RV, we approach smart contract security audits with a formal, mathematical outlook. We love formal methods! And we would like to share our passion for formal verification with the Algorand community. We believe that having a formal semantics of AVM and TEAL will wider adoption of formal verification among TEAL and PyTeal smart contract developers and auditors.

Our expertise

Runtime Verification Inc is a leading security audit service provider for smart contracts, and the Algorand Foundation's Security Partner. Besides traditional security audits, we have extensive experience of applying the K Framework to building mechanised formal proofs of smart contract correctness. The KEVM semantics of the Ethereum Virtual Machine is the bedrock of our verification toolchain for Ethereum smart contracts.

Project Scope and Timeline

Scope

We envision the semantics to take as input the following:

• an Algorand blockchain state, i.e. the lists and states of Accounts, ASAs and Applications;
• a description of an atomic transaction group;

and perform the group's evaluation. The result should be either approval and the commitment of the new, altered blockchain state, or denial and the rollback to the previous valid state before group evaluation.

Note that, at least for now, we do not intend to model the evaluation of several transaction groups or the wider Algorand consensus.

Timeline

We plan to achieve the project goals in three phases:

Discovery phase, 2 weeks

Over the past year, we have accumulated a number of internal developments, both in K and other languages, that model TEAL. Additionally, we have developed semantics in K for other blockchain virtual machines. We need to consolidate the knowledge and develop the semantics architecture in K.

Deliverables: Semantics architecture, description of the data structures and algorithms in form of flowcharts and natural language descriptions.

Development phase, 6 weeks

Following the architecture developed in the discovery phase, we will develop the semantics as a collection of K Framework modules. We will implement the semantics if every TEAL opcode, the execution cycle of a single TEAL transaction and the execution cycle of an atomic transaction group. We will work closely with the implements of KEVM to make use of their experience.

Deliverables: A complete and executable semantics of TEAL in K Framework. Unit-tests and symbolic proofs for individual opcode semantics. Limited integration tests in form of simple TEAL programs.

Testing and Validation phase, 6 weeks

Having the complete semantics in place, we will work with our clients' real smart-contracts already deployed on Algorand Mainnet. We will develop specifications for the key security and functional correctness properties for the contracts and carry-out TEAL-level proofs.

Deliverables: A case-study of a real mainnet-launched smart contract verification.

[ehildenb]

It looks good, I would just make some things more specific on the application. So for example, on the "Implementation Phase", you can put something like the following. Also, I'm not sure if linking the GitHub issues is a good idea, maybe it's better ot just list these things, but at least we should cerate the github issues. The links will be blocked anyway because algorand-sc-semantics is closed.

Relevant Issues:

• Refactor KTeal architecture to accomodate latest AVM transaction group architecture (2 weeks):
• Implement remaining TEAL4 (1 week):
• Implement TEAL5 semantics (2 weeks):
• Implement AVM ?.? semantics (1 week):

And I would list some more specific examples in the testing phase. In particular, I would list 2 different types of examples:

Simple Functional Proofs (2 weeks):

The "Simple Functional Proofs" represent just us trying to make sure that doing simple proofs is very easy, and doesn't have to mention crazy amounts of state.

• Arithmetic functions (2 weeks): <link to GitHub issue with add(X, Y), mul(X, Y), div(X, Y), max(X, Y), etc...>
• Simple control-flow: <link to GitHub issue with nested if-statement program, sequential ifs, etc...>
• A simple loop: .

Larger Real-World Proof (4 weeks):

This is us stepping into a larger contract to do some real-world verification, but probably not a full-fledged client contract, something still relatively simple. For example, in Ethereum we always use an ERC20 as this example, what's the equivalent here?

• Real World Proof 1 (ERC20) (4 weeks):

[geo2a]

K Framework semantics of TEAL

Project Goal and Motivation

Goals

This project intends to build:

• a formal, executable and open-source semantics of TEAL available to everyone;
• through the Haskell backend of K, a formal verification tool for TEAL programs;
• through the LLVM backend of K, a simulation and unit-testing framework with the performance comparable to the reference implementation.

Non-goals

We do not intend to build a replacement of the existing Algorand node implementation, therefore the model does not encompass the block consensus and validation rewards.

Motivation

The Algorand DeFi ecosystem is experiencing a boom of new projects that utilise the platform's scalability and fast transaction finality. The developer community is vibrant, productive and supportive, as witnessed by the active developer-focused Discourd community with nearly two thousand active members and many active discussions on Twitter. We also see a major surge of requests for security audits of Algorand smart contracts. In response to that surge, the Algorand auditors team at RV has grown significantly over the past months. While the auditing services we provide for Algroand at the moment mostly comprise manual code review and pen-and-paper reasoning, we already have two clients (name them here?) requesting full mechanised formal verification of their smart contracts.

At RV, we approach smart contract security audits with a formal, mathematical outlook. We love formal methods! And we would like to share our passion for formal verification with the Algorand community. We believe that having a formal semantics of AVM and TEAL will wider adoption of formal verification among TEAL and PyTeal smart contract developers and auditors.

Our expertise

Runtime Verification Inc is a leading security audit service provider for smart contracts, and the Algorand Foundation's Security Partner. Besides traditional security audits, we have extensive experience of applying the K Framework to building mechanised formal proofs of smart contract correctness. The KEVM semantics of the Ethereum Virtual Machine is the bedrock of our verification toolchain for Ethereum smart contracts.

Project Scope

We envision the semantics to take as input the following:

• an Algorand blockchain state, i.e. the lists and states of Accounts, ASAs and Applications;
• a description of an atomic transaction group;

and perform the group's evaluation. The result should be either approval and the commitment of the new, altered blockchain state, or denial and the rollback to the previous valid state before group evaluation.

Note that, at least for now, we do not intend to model the evaluation of several transaction groups or the wider Algorand consensus.

Project Timeline

We plan to achieve the project goals in three phases:

Discovery phase (2 weeks)

Over the past year, we have accumulated a number of internal developments, both in K and other languages, that model TEAL. More specifically, We have an existing prototype semantics that model the execution of a single transaction and TEAL v3. Additionally, we have developed semantics in K for other blockchain virtual machines. We need to consolidate the knowledge and develop the semantics architecture in K.

Deliverables: Semantics architecture, description of the data structures and algorithms in form of flowcharts and natural language descriptions.

Development phase (6 weeks)

Following the architecture developed in the discovery phase, we will develop the semantics as a collection of K Framework modules. We will implement the semantics if every TEAL opcode, the execution cycle of a single TEAL transaction and the execution cycle of an atomic transaction group. We will work closely with the implements of KEVM to make use of their experience.

More specifically, we need to accomplish the following tasks:

• Bring the current unfinished KTeal (supports TEAL v3) semantics up-to-date with the architecture developed in the Discovery Phase (2 weeks)
• Implement remaining TEAL v4 opcodes (1 week)
• Implement inner transactions support (2 weeks)
• Implement remaining TEAL v5 opcodes (1 week)
• If there is time remaining, research the upcoming TEAL v6 features

Deliverables: A complete and executable semantics of TEAL in K Framework. Unit-tests for individual opcode semantics. Limited integration tests in form of simple TEAL programs.

Testing phase (4 weeks)

The testing phase will focus on enlarging the unit and integration test suite, and on adding symbolic proofs.

The symbolic proof development will proceed bottom-up:

• First, we will develop correctness proofs for arithmetic opcodes, such as add, mul, div, etc. We will consider both uint64 and byte versions (1 week).
• Second, we will work on proof of correctness of control-flow operations, such as conditional jumps, loops and procedure calls (1 week).
• Finally, we will verify a number of simple algorithms implemented in TEAL (2 weeks).

The purpose of the basic symbolic proof suite is to both serve as a sanity-check for the semantics, and to showcase the methodology of constructing specification for simple TEAL programs. It is essential for the specification to be clear and concise, and to only mention the state they absolutely must to. This becomes vital to retain ease of understanding as we scale up to larger proofs.

Deliverables: A substantial suite of concrete unit-tests and symbolic proofs of correctness of TEAL programs.

Case-study phase (4 weeks)

Having the complete semantics in place, we will battle-test it to verify a public mainnet-launched smart contract. We would like this effort to benefit the community; hence, we will pick a contract deployed by the Algorand Foundation. A good candidate is the Governance Rewards contract, which we have previously audited.

Deliverables: A case-study of a real mainnet-launched smart contract verification.

[ehildenb]

Wow, this looks great, thank you Georgy :)

[ehildenb]

Here is the grant application form itself:

---

• Project Name: KTeal Formal Semantics for Teal Code Verification
• Company / Organisation Name: Runtime Verification, Inc.
• Country: USA
• Region: North America
• Core Team:
  • Team lead: Georgy Lukyanov has extensive experience auditing TEAL code, and working on the KTeal semantics. Georgy's involvement to date with the project makes us confident on his ability to deliver.
  • Advisor/Oversight: Everett Hildenbrandt helped develop numerous K semantics in the past, include KEVM (https://github.com/kframework/evm-semantics) and KWasm (https://github.com/kframework/wasm-semantics). Both semantics have been used for real-world verification of smart-contract code.

---

• Grant Submission Category: Development Tools
• What is your Focus Area?: TEAL analysis and formal proofs
• Specify: KTEAL is for TEAL correctness proofs on critical parts of smart contracts.
• Website URL: https://github.com/runtimeverification/algorand-sc-semantics
• Short Description - One Liner (Tweet): https://runtimeverification.com/
• Elevator Pitch (Why should we fund you?): We do formal verification of EVM bytecode for clients that want even more assurance than a normal audit. Our current KTeal semantics is outdated because we have been busy auditing Teal code for the Algorand ecosystem, so we need to update it to Teal 6, which will require turning away audit engagements. Already we have two audit clients who have asked for formal verificaiton of their Teal code (CLIENT1 and CLIENT2), because they see that we offer that service for EVM bytecode.
• Provide The URL Of Your Project Repository: placeholder (need to open source)
• What Stage Is The Project In?: In Progress - We've got the ball rolling already
• Briefly Outline What's Left To Do: (i) Implement tracking of scratch spaces of previous transactions so that we can finish up the last two opcodes of Teal 4. (ii) Implement the remaining Teal 5, specifically inner transaction. (iii) Implement Teal 6. (iv) Use the semantics for some lightweight verification tasks to test out its suitability. (See attached PDF for more detailed information).
• Estimated Date of Project Completion: May 27, 2022
• Solution Approach:
• Technical Roadmap & Statement of Work:
• Key Milestones:
• What is Innovative about your Proposal?:
• Is this Project Open Source?:
• How does the project further Decentralization?:
• Describe your Technology Stack:
• Experience Building Blockchain Technology: We've a deep understanding of building DApps on Algorand
• Are you building on any other Layer1 Blockchain?: Ethereum, Tezos, Cardano, Polkadot, Cosmos
• Grant Amount Requested (In USD): 300000
• Estimated Total Cost of Project (In USD): 420000
• Have You Been Successful In Receiving A Grant From Us Before?: No
• Please Detail Any Other Sources Of Funding: None
• Is anyone on the team affiliated with a university and/or is the project planning to engage or collaborate with universities or university affiliates?: No
• Please Upload Your Budget & Cost Projection:

---

• What is your Twitter Handle?: @rv_inc
• What is your Discord Username?: geo2a#4262
• What is your Telegram Username?: @geo2a
• How Did You Hear About Our Grants Program?: Referral
• Contact Name of Referral : Ryan Terribilini
• Please Upload a Logo: @bogdan-stanciu can you post an RV logo we can use?
• Investor Deck/Additional Information:

[bogdan-stanciu]

[geo2a]

Looks good @ehildenb! A small correction:

Briefly Outline What's Left To Do: (i) Implement the more general "inner transactions" of Teal 4 ...

The inner transaction are a feature of Teal 5. Let's write this: "(i) Implement tracking of scratch spaces of previous transactions so that we can finish up the last two opcodes of Teal 4. (ii) Implement the remaining Teal 5, specifically inner transaction." and the rest as you wrote.

My Discord handle, as shown on my settings screen, is geo2a#4262. I am not sure that "#4262" is required, I'm not that familiar with Discord.

I do not think we have an active telegram group related to this project, or do you mean something else? My handle is @geo2a too on Telegram.

[geo2a]

@ehildenb I've also taken a look at Algorand Foundation grant recipients page, and I see RV there, see this post. Looks like they treat our AlgoClarity retainer agreement as a grant? I don't know if you're aware of that. Hence, the claim that we have not received a grant from them before may be wrong.

[ChristianoBraga]

Here is the grant application form itself:

---

• Project Name: KTeal Formal Semantics for Teal Code Verification
• Company / Organisation Name: Runtime Verification, Inc.
• Country: USA
• Region: North America
• Core Team:
  • Team lead: Georgy Lukyanov has extensive experience auditing TEAL code, and working on the KTeal semantics. Georgy's involvement to date with the project makes us confident on his ability to deliver.
  • Advisor/Oversight: Everett Hildenbrandt helped develop numerous K semantics in the past, include KEVM (https://github.com/kframework/evm-semantics) and KWasm (https://github.com/kframework/wasm-semantics). Both semantics have been used for real-world verification of smart-contract code.

---

• Grant Submission Category: Development Tools

• What is your Focus Area?: TEAL analysis and formal proofs

• Specify: KTEAL is for TEAL correctness proofs on critical parts of smart contracts.

• Website URL: https://github.com/runtimeverification/algorand-sc-semantics

• Short Description - One Liner (Tweet): https://runtimeverification.com/

• Elevator Pitch (Why should we fund you?): We do formal verification of EVM bytecode for clients that want even more assurance than a normal audit. Our current KTeal semantics is outdated because we have been busy auditing Teal code for the Algorand ecosystem, so we need to update it to Teal 6, which will require turning away audit engagements. Already we have two audit clients who have asked for formal verificaiton of their Teal code (CLIENT1 and CLIENT2), because they see that we offer that service for EVM bytecode.

• Provide The URL Of Your Project Repository: placeholder (need to open source)

• What Stage Is The Project In?: In Progress - We've got the ball rolling already

• Briefly Outline What's Left To Do: (i) Implement tracking of scratch spaces of previous transactions so that we can finish up the last two opcodes of Teal 4. (ii) Implement the remaining Teal 5, specifically inner transaction. (iii) Implement Teal 6. (iv) Use the semantics for some lightweight verification tasks to test out its suitability. (See attached PDF for more detailed information).

• Estimated Date of Project Completion: May 27, 2022

• Solution Approach:

• Technical Roadmap & Statement of Work:

  • Goals
    This project intends to build:
  • a formal, executable and open-source semantics of TEAL available to everyone;
  • through the Haskell backend of K, a formal verification tool for TEAL programs;
  • through the LLVM backend of K, a simulation and unit-testing framework with the performance comparable to the reference implementation.
  • Non-goals
    We do not intend to build a replacement of the existing Algorand node implementation, therefore the model does not encompass the block consensus and validation rewards.
  • Motivation
    The Algorand DeFi ecosystem is experiencing a boom of new projects that utilise the platform's scalability and fast transaction finality. The developer community is vibrant, productive and supportive, as witnessed by the active developer-focused Discourd community with nearly two thousand active members and many active discussions on Twitter. We also see a major surge of requests for security audits of Algorand smart contracts. In response to that surge, the Algorand auditors team at RV has grown significantly over the past months. While the auditing services we provide for Algroand at the moment mostly comprise manual code review and pen-and-paper reasoning, we already have two clients (name them here?) requesting full mechanised formal verification of their smart contracts.
  • Project Scope
    We envision the semantics to take as input the following:
  • an Algorand blockchain state, i.e. the lists and states of Accounts, ASAs and Applications;
  • a description of an atomic transaction group; and perform the group's evaluation. The result should be either approval and the commitment of the new, altered blockchain state, or denial and the rollback to the previous valid state before group evaluation. Note that, at least for now, we do not intend to model the evaluation of several transaction groups or the wider Algorand consensus.
  • Discovery phase (2 weeks). Over the past year, we have accumulated a number of internal developments, both in K and other languages, that model TEAL. More specifically, We have an existing prototype semantics that model the execution of a single transaction and TEAL v3. Additionally, we have developed semantics in K for other blockchain virtual machines. We need to consolidate the knowledge and develop the semantics architecture in K. Deliverables: Semantics architecture, description of the data structures and algorithms in form of flowcharts and natural language descriptions.
  • Development phase (6 weeks) Following the architecture developed in the discovery phase, we will develop the semantics as a collection of K Framework modules. We will implement the semantics if every TEAL opcode, the execution cycle of a single TEAL transaction and the execution cycle of an atomic transaction group. We will work closely with the implements of KEVM to make use of their experience.
    More specifically, we need to accomplish the following tasks:
  • Bring the current unfinished KTeal (supports TEAL v3) semantics up-to-date with the architecture developed in the Discovery Phase (2 weeks)
  • Implement remaining TEAL v4 opcodes (1 week)
  • Implement inner transactions support (2 weeks)
  • Implement remaining TEAL v5 opcodes (1 week)
  • If there is time remaining, research the upcoming TEAL v6 features Deliverables: A complete and executable semantics of TEAL in K Framework. Unit-tests for individual opcode semantics. Limited integration tests in form of simple TEAL programs.
  • Testing phase (4 weeks) The testing phase will focus on enlarging the unit and integration test suite, and on adding symbolic proofs.
    The symbolic proof development will proceed bottom-up:
    • First, we will develop correctness proofs for arithmetic opcodes, such as add, mul, div, etc. We will consider both uint64 and byte versions (1 week).
    • Second, we will work on proof of correctness of control-flow operations, such as conditional jumps, loops and procedure calls (1 week).
    • Finally, we will verify a number of simple algorithms implemented in TEAL (2 weeks).
      The purpose of the basic symbolic proof suite is to both serve as a sanity-check for the semantics, and to showcase the methodology of constructing specification for simple TEAL programs. It is essential for the specification to be clear and concise, and to only mention the state they absolutely must to. This becomes vital to retain ease of understanding as we scale up to larger proofs.
      Deliverables: A substantial suite of concrete unit-tests and symbolic proofs of correctness of TEAL programs.
  • Case-study phase (4 weeks) Having the complete semantics in place, we will battle-test it to verify a public mainnet-launched smart contract. We would like this effort to benefit the community; hence, we will pick a contract deployed by the Algorand Foundation. A good candidate is the Governance Rewards contract, which we have previously audited. Deliverables: A case-study of a real mainnet-launched smart contract verification.

• Key Milestones:

  • Informal description of TEAL structures and behavior.
  • A formal semantics for TEAL in K.
  • A proof suite for TEAL.
  • A verified real-world-sized TEAL contract verified in KTEAL.

• What is Innovative about your Proposal?: Runtime Verification Inc is a leading security audit service provider for smart contracts, and the Algorand Foundation's Security Partner. Besides traditional security audits, we have extensive experience of applying the K Framework to building mechanised formal proofs of smart contract correctness. The KEVM semantics of the Ethereum Virtual Machine is the bedrock of our verification toolchain for Ethereum smart contracts.
  At RV, we approach smart contract security audits with a formal, mathematical outlook. We love formal methods! And we would like to share our passion for formal verification with the Algorand community. We believe that having a formal semantics of AVM and TEAL will wider adoption of formal verification among TEAL and PyTeal smart contract developers and auditors.

• Is this Project Open Source?: Yes

• How does the project further Decentralization?: This project offers high quality audits to the TEAL ecosystem, and that requires a semantics in order to create a solid foundation that will allow for the development of analysis and audit tools for TEAL. Developing semantics is expensive thus the grant becomes essential for us to provide formally-based high-quality services to the TEAL community. Moreover, in terms of community effect, this project will produce an open source semantics which anyone can use to do program verification, and will be used to offer formal verification for key projects in the TEAL ecosystem. The k-dss project is a fair example of an open source semantics (KEVM) leading to real community value (securing Dai smart contracts).

• Describe your Technology Stack: The K framework is a language-agnostic formal tool for the development of programming languages tools. It encompasses many components developed in different languages carefully chosen to develop each component. Some of them are:

  • K front-end: it defines a notation for rule-based specifications.
  • Kore: is the intermediate representation of K. It is essentially a concrete syntax for matching logic, the logic foundation of K. K definitions are compiled to Kore.
  • K's backends: the main backends today are comprised by the LLVM backend and the Haskell backend. The former provides efficient execution and state search capabilities to Kore definitions and the latter provides a fully-fledged symbolic machine to K. The Haskell backend in connection with an SMT solver give rise to a powerful theorem prover. The K approach to language-development encompasses the development of a formal semantics as a K description which is then used as the formal theory upon which properties of programs are done.

• Experience Building Blockchain Technology: We've a deep understanding of building DApps on Algorand.

• Are you building on any other Layer1 Blockchain?: Ethereum, Tezos, Cardano, Polkadot, and Cosmos.

• Grant Amount Requested (In USD): 300000

• Estimated Total Cost of Project (In USD): 420000

• Have You Been Successful In Receiving A Grant From Us Before?: Yes, it can be seen here.

• Please Detail Any Other Sources Of Funding: None

• Is anyone on the team affiliated with a university and/or is the project planning to engage or collaborate with universities or university affiliates?: No

• Please Upload Your Budget & Cost Projection:

---

• What is your Twitter Handle?: @rv_inc
• What is your Discord Username?: geo2a#4262
• What is your Telegram Username?: @geo2a
• How Did You Hear About Our Grants Program?: Referral
• Contact Name of Referral : Ryan Terribilini
• Please Upload a Logo:
• Investor Deck/Additional Information:

[malturki]

This proposal has just been submitted to Algorand Foundation through their $10 Million Dev Tooling SupaGrant program. Below are the contents of the form for reference.

---

• Organization / Company Name: Runtime Verification, Inc.

• Project Name: KTEAL: Formal Semantics for TEAL Smart Contract Analysis and Verification

• Core Team & Experience: Team lead: Georgy Lukyanov (Github: geo2a) has extensive experience auditing TEAL code, working on the KTEAL semantics and TEAL/PyTEAL analysis tools. Georgy's involvement to date with the project makes us confident on his ability to deliver. Advisor/Oversight: Everett Hildenbrandt (Github: ehildenb) helped develop numerous K semantics in the past, include KEVM (https://github.com/kframework/evm-semantics) and KWasm (https://github.com/kframework/wasm-semantics). Both semantics have been used for real-world verification of smart-contract code.

• Short Project Description: The development of formal analysis and verification tools for TEAL enabling concrete and symbolic execution, model-based testing and test coverage analysis, and correctness proofs on critical parts of TEAL smart contracts.

• Elevator Pitch (up to 400 characters): Formally verifying correctness provides the highest levels of assurance. We provide formal-verification-based auditing services of EVM bytecode, which add significant value to developers and the ecosystem. Already we have audit clients who have asked for formal verification of their TEAL code. The project enables providing these services and allows developers to deploy provably correct code.

• What Stage Is The Project In?: We have a preliminary and incomplete prototype in K of TEAL v3 already developed and usable. The prototype can be used to run simple TEAL v3 contracts and prove some simple reachability properties.

• Grant Amount Requested (In USD): 300000

• Estimated Total Cost of Project (In USD): 420000

• Provide The URL Of Your Project Repository: https://github.com/runtimeverification/avm-semantics [Note: currently a private Github repo]

• Are you building on any other layer 1 blockchain?: Yes: Ethereum, Tezos, Cardano, Polkadot, and Cosmos.

• What is your Website URL (if applicable)?: https://runtimeverification.com/

• Primary Contact: Patrick MacKay, COO at Runtime Verification, patrick.mackay@runtimeverification.com

• Contact Name of Referral: Ryan Terribilini

• Where did you hear about SupaGrants?: Friends and Twitter

Company Description

Runtime Verification Inc. is a technology startup headquartered in the USA with staff spread across the globe, including Europe, South America, and Southeast Asia. We provide testing and verification services to public and private companies in the embedded and blockchain domains. In the latter we work with infrastructure builders as well as companies building products and providing services supported and/or powered by said infrastructure. The company was founded in 2010. It employs 50 people at the moment, and is looking to double in size in the next 12 to 18 months.

For the time being, blockchain safety tests are mostly lightweight static analysis tests (testing only the internal logic of source code), while dynamic analysis test (using the data generated as the codes are compiled and executed) increases coverage to find bugs as opposed to static analysis tests. Runtime Verification is a global leader in formal verification and is capable of directly verifying compiled binary code. Compared to the formal verification of source code, this catches bugs that are otherwise missed due to miscompilation.

Provide a Technical Description of Your Solution

The solution is based on developing formal specifications of the TEAL language and TEAL's execution engine in the AVM in the K framework and deriving all artifacts and analysis tools from these specifications. The K framework is a language-agnostic formal tool for the development of programming languages tools. It encompasses many components developed in different languages carefully chosen to develop each component. Some of them are:

• K front-end: it defines a notation for rule-based specifications.
• Kore: is the intermediate representation of K. It is essentially a concrete syntax for matching logic, the logic foundation of K. K definitions are compiled to Kore.
• K's backends: the main backends today are comprised by the LLVM backend and the Haskell backend. The former provides efficient execution and state search capabilities to Kore definitions and the latter provides a fully-fledged symbolic machine to K. The Haskell backend in connection with an SMT solver give rise to a powerful theorem prover.
• The K approach to language-development encompasses the development of a formal semantics as a K description which is then used as the formal theory upon which properties of programs are done.

Technical Roadmap & Statement of Work

Motivation:

The Algorand DeFi ecosystem is experiencing a boom of new projects that utilise the platform's scalability and fast transaction finality. The developer community is vibrant, productive and supportive, as witnessed by the active developer-focused Discord community with nearly two thousand active members and many active discussions on Twitter. We also see a major surge of requests for security audits of Algorand smart contracts.

Runtime Verification Inc is a leading security audit service provider for smart contracts, and the Algorand Foundation's Security Partner. The Algorand auditors team at RV has grown significantly over the past months, primarily in response to this surge in audit requests. While the auditing services we provide for Algroand at the moment mostly comprise manual code review and pen-and-paper reasoning, we already have clients approaching us and requesting full mechanised formal verification of their smart contracts. Besides traditional security audits, we have extensive experience of applying the K Framework to building mechanised formal proofs of smart contract correctness. The KEVM semantics of the Ethereum Virtual Machine is the bedrock of our verification toolchain for Ethereum smart contracts.

At RV, we approach smart contract security audits with a formal, mathematical outlook. We love formal methods! And we would like to share our passion for formal verification with the Algorand community. We believe that having a formal semantics of AVM and TEAL will widen adoption of formal verification among TEAL and PyTeal smart contract developers and auditors. Developing semantics is expensive though, and thus the grant becomes essential for us to provide formally-based high-quality services to the TEAL community. Moreover, in terms of community effect, this project will produce an open source semantics which anyone (developers, researchers, auditing firms, ... etc) can use to do program verification, and will be used to offer formal verification for key projects in the TEAL ecosystem. The k-dss project is a fair example of an open source semantics (KEVM) leading to real community value (securing DAI smart contracts).

Goals:

This project intends to build:

1. a formal, executable and open-source semantics of TEAL available to everyone;
2. through the Haskell backend of K, a symbolic execution engine and a formal verification tool for TEAL smart contracts;
3. through the LLVM backend of K, a simulation and unit-testing framework (with coverage analysis) with performance that is comparable to that of the reference implementation.

Non-goals:

We do not intend to build a replacement of the existing Algorand node implementation, therefore the model does not encompass the block consensus and validation rewards.

Project Scope:

We envision the semantics to take as input the following:

1. an Algorand blockchain state, i.e. the lists and states of Accounts, ASAs and Applications;
2. a description of an atomic transaction group; and perform the group's evaluation. The result should be either approval and the commitment of the new, altered blockchain state, or denial and the rollback to the previous valid state before group evaluation (see the attached TEAL execution flowchart). Note that, at least for now, we do not intend to model the evaluation of several transaction groups or the wider Algorand consensus.

Project Phases and Timeline:

1. Discovery phase (2 weeks). Over the past year, we have accumulated a number of internal developments, both in K and other languages, that model TEAL. More specifically, We have an existing prototype semantics that model the execution of a single transaction and TEAL v3. Additionally, we have developed semantics in K for other blockchain virtual machines. We need to consolidate the knowledge and develop a semantics architecture in the K framework that supports current (and future) versions of TEAL and the AVM. Deliverables: Semantics architecture, description of the data structures and algorithms in form of flowcharts and natural language descriptions.

2. Development phase (7 weeks). Following the architecture developed in the discovery phase, we will develop the semantics as a collection of K Framework modules. We will implement the semantics of all TEAL opcodes, the execution cycle of a single TEAL transaction and the execution cycle of an atomic transaction group. We will work closely with the implementors of KEVM to make use of their experience. More specifically, we need to accomplish the following tasks:

   • Bring the current unfinished KTEAL semantics (which supports TEAL v3) up-to-date with the architecture developed in the Discovery Phase (2 weeks)
   • Implement remaining TEAL v4 opcodes (1 week)
   • Implement inner transactions support (2 weeks)
   • Implement remaining TEAL v5 opcodes (1 week)
   • research and implement the recently added TEAL v6 features (1 week) Deliverables: A complete and executable semantics of TEAL in K Framework. Unit-tests for individual opcode semantics. Limited integration tests in form of simple TEAL programs.

3. Testing phase (4 weeks) The testing phase will focus on enlarging the unit and integration test suite, and on adding symbolic proofs. The symbolic proof development will proceed bottom-up:

   • First, we will develop correctness proofs for arithmetic opcodes, such as add, mul, div, etc. We will consider both uint64 and byte versions (1 week).
   • Second, we will work on proofs of correctness of control-flow operations, such as conditional jumps, loops and procedure calls (1 week).
   • Finally, we will verify a number of simple algorithms implemented in TEAL (2 weeks). The purpose of the basic symbolic proof suite is to both serve as a sanity-check for the semantics, and to showcase the methodology of constructing specification for simple TEAL programs. It is essential for the specification to be clear and concise, and to only mention the state they absolutely must refer to. This becomes vital to retain ease of understanding as we scale up to larger proofs. Deliverables: A substantial suite of concrete unit-tests and symbolic proofs of correctness of TEAL programs.

4. Case-study phase (4 weeks) Having the complete semantics in place, we will battle-test it to verify a public mainnet-launched smart contract. We would like this effort to benefit the community; hence, we will pick a contract deployed by the Algorand Foundation. A good candidate is the Governance Rewards contract, which we have previously audited. Deliverables: A case-study of a real mainnet-launched smart contract verification.

Key Milestones:

There is one key milestone for each project phase as described above. The key milestones are as follows:

• (2 weeks) Informal description of the semantics architecture of TEAL and its structures and behavior
• (7 weeks) An executable, formal semantics for TEAL in K along with a set of tools (interpreter, symbolic execution engine, formal verifier)
• (4 weeks) A test suite and a proof suite for TEAL (with documentation)
• (4 weeks) A verified real-world-sized TEAL contract verified in KTEAL

[geo2a]

The current version of the grant application is maintained at https://github.com/runtimeverification/avm-semantics/blob/master/docs/algo-grant-application.md