Musab A. Alturki, PhD

Musab A. Alturki, PhD

Senior Research Engineer @ Runtime Verification Inc. working on formal modeling and verification of blockchain and distributed systems

Posts by Tags

Algorand

Best Practices For Securing Algorand Smart Contracts

less than 1 minute read

Published:

Smart contracts are the backbone of decentralized applications in Algorand. Ensuring their security against attacks and the safety of funds they maintain is critical to the success of these applications. In this talk, we give an overview of our world-class security auditing services at Runtime Verification, and reflect on our experiences auditing TEAL smart contracts in Algorand. We highlight some common programming pitfalls and provide some recommendations for best practices when developing TEAL smart contracts.

Added support for TEAL 5 in Tealer

less than 1 minute read

Published:

Tealer is a static analysis tool developed by Trail of Bits for analyzing the structure of smart contracts written in TEAL. I have added to Tealer support for the new features introduced in TEAL 5, including inner transactions.

Runtime Verification Audits Tinyman

less than 1 minute read

Published:

Runtime Verification announced Tinyman’s audit completioni, which was an effort I’ve had the pleasure of leading. Tinyman is a new project under development that focuses on bringing a decentralized trading protocol to the Algorand ecosystem and its community.

Announcement

Runtime Verification Audits Tinyman

less than 1 minute read

Published:

Runtime Verification announced Tinyman’s audit completioni, which was an effort I’ve had the pleasure of leading. Tinyman is a new project under development that focuses on bringing a decentralized trading protocol to the Algorand ecosystem and its community.

Beacon Chain

Formally Verifying Finality in Gasper: The Core of the Beacon Chain

less than 1 minute read

Published:

Gasper is an abstract proof-of-stake protocol layer that is implemented by the Beacon Chain protocol, the underlying protocol of the upcoming Ethereum 2.0 network. This post highlights our achievements in formally proving key correctness properties of finality in Gasper using the Coq proof assistant.

Casper

Formally Verifying Finality in Gasper: The Core of the Beacon Chain

less than 1 minute read

Published:

Gasper is an abstract proof-of-stake protocol layer that is implemented by the Beacon Chain protocol, the underlying protocol of the upcoming Ethereum 2.0 network. This post highlights our achievements in formally proving key correctness properties of finality in Gasper using the Coq proof assistant.

Coq

Formally Verifying Finality in Gasper: The Core of the Beacon Chain

less than 1 minute read

Published:

Gasper is an abstract proof-of-stake protocol layer that is implemented by the Beacon Chain protocol, the underlying protocol of the upcoming Ethereum 2.0 network. This post highlights our achievements in formally proving key correctness properties of finality in Gasper using the Coq proof assistant.

K vs. Coq as Language Verification Frameworks

less than 1 minute read

Published:

Ever wondered how K and Coq compare and contrast as language verification frameworks? I posted a series of articles comparing K and Coq as language verification frameworks through a working example.

Editor

Ethereum

Formally Verifying Finality in Gasper: The Core of the Beacon Chain

less than 1 minute read

Published:

Gasper is an abstract proof-of-stake protocol layer that is implemented by the Beacon Chain protocol, the underlying protocol of the upcoming Ethereum 2.0 network. This post highlights our achievements in formally proving key correctness properties of finality in Gasper using the Coq proof assistant.

Formal Verification

Best Practices For Securing Algorand Smart Contracts

less than 1 minute read

Published:

Smart contracts are the backbone of decentralized applications in Algorand. Ensuring their security against attacks and the safety of funds they maintain is critical to the success of these applications. In this talk, we give an overview of our world-class security auditing services at Runtime Verification, and reflect on our experiences auditing TEAL smart contracts in Algorand. We highlight some common programming pitfalls and provide some recommendations for best practices when developing TEAL smart contracts.

Runtime Verification Audits Tinyman

less than 1 minute read

Published:

Runtime Verification announced Tinyman’s audit completioni, which was an effort I’ve had the pleasure of leading. Tinyman is a new project under development that focuses on bringing a decentralized trading protocol to the Algorand ecosystem and its community.

Formally Verifying Finality in Gasper: The Core of the Beacon Chain

less than 1 minute read

Published:

Gasper is an abstract proof-of-stake protocol layer that is implemented by the Beacon Chain protocol, the underlying protocol of the upcoming Ethereum 2.0 network. This post highlights our achievements in formally proving key correctness properties of finality in Gasper using the Coq proof assistant.

K vs. Coq as Language Verification Frameworks

less than 1 minute read

Published:

Ever wondered how K and Coq compare and contrast as language verification frameworks? I posted a series of articles comparing K and Coq as language verification frameworks through a working example.

Gasper

Formally Verifying Finality in Gasper: The Core of the Beacon Chain

less than 1 minute read

Published:

Gasper is an abstract proof-of-stake protocol layer that is implemented by the Beacon Chain protocol, the underlying protocol of the upcoming Ethereum 2.0 network. This post highlights our achievements in formally proving key correctness properties of finality in Gasper using the Coq proof assistant.

K

K Framework

K vs. Coq as Language Verification Frameworks

less than 1 minute read

Published:

Ever wondered how K and Coq compare and contrast as language verification frameworks? I posted a series of articles comparing K and Coq as language verification frameworks through a working example.

Kakoune

Maude

Programming Languages

K vs. Coq as Language Verification Frameworks

less than 1 minute read

Published:

Ever wondered how K and Coq compare and contrast as language verification frameworks? I posted a series of articles comparing K and Coq as language verification frameworks through a working example.

RANDAO

Security Audit

Best Practices For Securing Algorand Smart Contracts

less than 1 minute read

Published:

Smart contracts are the backbone of decentralized applications in Algorand. Ensuring their security against attacks and the safety of funds they maintain is critical to the success of these applications. In this talk, we give an overview of our world-class security auditing services at Runtime Verification, and reflect on our experiences auditing TEAL smart contracts in Algorand. We highlight some common programming pitfalls and provide some recommendations for best practices when developing TEAL smart contracts.

Added support for TEAL 5 in Tealer

less than 1 minute read

Published:

Tealer is a static analysis tool developed by Trail of Bits for analyzing the structure of smart contracts written in TEAL. I have added to Tealer support for the new features introduced in TEAL 5, including inner transactions.

Runtime Verification Audits Tinyman

less than 1 minute read

Published:

Runtime Verification announced Tinyman’s audit completioni, which was an effort I’ve had the pleasure of leading. Tinyman is a new project under development that focuses on bringing a decentralized trading protocol to the Algorand ecosystem and its community.

Smart Contracts

Best Practices For Securing Algorand Smart Contracts

less than 1 minute read

Published:

Smart contracts are the backbone of decentralized applications in Algorand. Ensuring their security against attacks and the safety of funds they maintain is critical to the success of these applications. In this talk, we give an overview of our world-class security auditing services at Runtime Verification, and reflect on our experiences auditing TEAL smart contracts in Algorand. We highlight some common programming pitfalls and provide some recommendations for best practices when developing TEAL smart contracts.

Added support for TEAL 5 in Tealer

less than 1 minute read

Published:

Tealer is a static analysis tool developed by Trail of Bits for analyzing the structure of smart contracts written in TEAL. I have added to Tealer support for the new features introduced in TEAL 5, including inner transactions.

Runtime Verification Audits Tinyman

less than 1 minute read

Published:

Runtime Verification announced Tinyman’s audit completioni, which was an effort I’ve had the pleasure of leading. Tinyman is a new project under development that focuses on bringing a decentralized trading protocol to the Algorand ecosystem and its community.

Static analysis

Added support for TEAL 5 in Tealer

less than 1 minute read

Published:

Tealer is a static analysis tool developed by Trail of Bits for analyzing the structure of smart contracts written in TEAL. I have added to Tealer support for the new features introduced in TEAL 5, including inner transactions.

Syntax Highlighting

Talks

Best Practices For Securing Algorand Smart Contracts

less than 1 minute read

Published:

Smart contracts are the backbone of decentralized applications in Algorand. Ensuring their security against attacks and the safety of funds they maintain is critical to the success of these applications. In this talk, we give an overview of our world-class security auditing services at Runtime Verification, and reflect on our experiences auditing TEAL smart contracts in Algorand. We highlight some common programming pitfalls and provide some recommendations for best practices when developing TEAL smart contracts.

Tealer

Added support for TEAL 5 in Tealer

less than 1 minute read

Published:

Tealer is a static analysis tool developed by Trail of Bits for analyzing the structure of smart contracts written in TEAL. I have added to Tealer support for the new features introduced in TEAL 5, including inner transactions.