Sitemap

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

Posts

Best Practices For Securing Algorand Smart Contracts

less than 1 minute read

Published: November 30, 2021

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: October 24, 2021

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: September 21, 2021

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.

A K Syntax Highlighter for the Kakoune Text Editor

less than 1 minute read

Published: October 15, 2020

Basic syntax highlighting for K (the K Framework) in the Kakoune text editor.

Runtime Verification and Algorand announce a new engagement to build formal tools for Algorand’s smart contract ecosystem

less than 1 minute read

Published: July 28, 2020

Runtime Verification has been awarded a grant by Algorand Foundation to develop a formal semantic framework for Algorand’s smart contracts using the K framework.

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

less than 1 minute read

Published: July 15, 2020

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: December 12, 2019

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.

A Formal Model in K of the Beacon Chain

less than 1 minute read

Published: October 22, 2019

I posted an article celebrating the successful completion of the first milestone in an ongoing collaboration between Runtime Verification and Ethereum Foundation, to build a formal framework for modeling and verifying the Beacon Chain. We have completed the executable formal model of Beacon Chain in the K Framework.

Two Papers Presented at FMBC’19

less than 1 minute read

Published: October 11, 2019

We have two papers presented today at the 1st Workshop on Formal Methods for Blockchains, hosted by the 3rd Formal Methods World Congress on October 11, 2019 in Porto, Portugal:

Formally Modeling Algorand and Verifying its Safety Property

less than 1 minute read

Published: June 18, 2019

I posted an article celebrating the successful completion of the first part of an ongoing collaboration between Runtime Verification and Algorand, to model Algorand’s consensus protocol and verify its safety theorem using the Coq proof assistant].

projects

Modeling and Verification Distance Fraud Attacks

Statistical model checking of distance fraud attacks on the Hancke-Kuhn family of protocols

Resource-bounded Intruders in Denial of Service Attacks

A formal resource-bounded-intruders model for a wide range of denial of service attacks

Statistical Model Checking of RANDAO Against Attacks

Statistical model checking of RANDAO’s resilience against pre-computed reveal sstrategies

Verification of Algorand’s Safety Property

Modeling of the Algorand Consensus Protocol in the Coq proof assistant and verifying its safety guarantees

An executable model of the Beacon Chain protocol

An executable K model of Ethereum 2.0 Beacon Chain Phase 0 specification

Modeling and Verification of Gasper

Modeling Gasper and verifying its properties using the Coq proof assistant

Formal tooling for Algorand’s smart contract architecture

Building formal semantics of both L1 and L2 languages for Algorand’s smart contract architecture in the K framework

publications

Real-Time Rewriting Semantics of Orc

Principles and Practice of Declarative Programming, ACM, pp 131–142, 2007

Musab A. Alturki and José Meseguer

Reduction Semantics and Formal Analysis of Orc Programs

Automated Specification and Verification of Web Systems, ENTCS 200, pp 25–41, 2008

Musab A. Alturki and José Meseguer

PBES: A Policy Based Encryption System with Application to Data Sharing in the Power Grid

International Symposium on Information, Computer, and Communications Security, ACM, pp 262-275, 2009

Rakesh Bobba, Himanshu Khurana, Musab A. Alturki and Farhana Ashraf

Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol

Security and Rewriting Techniques, ENTCS 234, pp 3-18, 2009

Musab A. Alturki, José Meseguer and Carl A. Gunter

Formal Specification and Analysis of Timing Properties in Software Systems

Fundamental Approaches to Software Engineering, Springer, LNCS 5503, pp 262-277, 2009

Musab A. Alturki, Dinakar Dhurjati, Dachuan Yu, Ajay Chander and Hiroshi Inamura

Model-Checking DoS Amplification for VoIP Session Initiation

European Symposium on Research in Computer Security, Springer, LNCS 5789, pp 390-405, 2009

Ravinder Shankesi, Musab A. Alturki, Ralf Sasse, Carl A. Gunter and José Meseguer

Dist-Orc: A Rewriting-based Distributed Implementation of Orc with Formal Analysis

Rewriting Techniques for Real-Time Systems, EPTCS 36, pp 26-45, 2010

Musab A. Alturki and José Meseguer

PVeStA: A Parallel Statistical Model Checking and Quantitative Analysis Tool

Algebra and Coalgebra in Computer Science, Springer, LNCS 6859, pp 386-392, 2011

Musab A. Alturki and José Meseguer

Stable Availability under Denial of Service Attacks through Formal Patterns

Fundamental Approaches to Software Engineering, Springer, LNCS 7212, pp 78-93, 2012

Jonas Eckhardt, Tobias Mühlbauer, Musab A. Alturki, José Meseguer and Martin Wirsing

Sparse Single-Hidden Layer Feedforward Network for Mapping Natural Language Questions to SQL Queries

Artificial Neural Networks and Machine Learning, Springer, LNCS 8681, pp 241-248, 2014

Issam H. Laradji, Lahouari Ghouti, Faisal Saleh and Musab A. Alturki

Towards Formal Verification of Orchestration Computations Using the K Framework

Formal Methods, Springer, LNCS 9109, pp 40-56, 2015

Musab A. Alturki and Omar Alzuhaibi

Executable Rewriting Logic Semantics of Orc and Formal Analysis of Orc Programs

Journal of Logical and Algebraic Methods in Programming, Volume 84(4), pp 505–533, 2015

Musab A. Alturki and José Meseguer

Implementing the Observer Design Pattern as an Expressive Language Construct

Software Engineering Advances, pp 463-469, 2015

Taher A. Ghaleb, Khalid Aljasser and Musab A. Alturki

A Symbolic Rewriting Semantics of the COMPASS Modeling Language

Information Reuse and Integration, IEEE, pp 283-290, 2017

Musab A. Alturki

Statistical Model Checking of Distance Fraud Attacks on the Hancke-Kuhn Family of Protocols

Cyber-Physical Systems Security and Privacy, ACM, pp 60-71, 2018

Musab A. Alturki, Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov and Carolyn Talcott

Program Comprehension through Reverse-engineered Sequence Diagrams: A Systematic Review

Journal of Software: Evolution and Process, Wiley, Volume 30(11), pp e1965, 2018

Taher A. Ghaleb, Musab A. Alturki and Khalid Aljasser

A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols

Foundations of Security, Protocols, and Equational Reasoning, Springer, LNCS 11565, pp 192-213, 2019

Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich, Vivek Nigam, Andre Scedrov and Carolyn Talcott

Resource-Bounded Intruders in Denial of Service Attacks

Computer Security Foundations Symposium, IEEE, pp 382-396, 2019

Abraão Aires Urquiza, Musab A. Alturki, Max Kanovich, Tajana Ban Kirigin, Vivek Nigam, Andre Scedrov and Carolyn Talcott

Towards a Verified Model of the Algorand Consensus Protocol in Coq

Proceedings of Formal Methods (FM) 2019 International Workshops, volume 12232 of LNCS, pages 362-367, 2020

Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña and Grigore Roşu

Statistical Model Checking of RANDAO’s Resilience to Pre-computed Reveal Strategies

Formal Methods (FM) 2019 International Workshops, volume 12232 of LNCS, pages 337–349, 2020

Musab A. Alturki and Grigore Roşu

Enhanced Visualization of Method Invocations by Extending Reverse-engineered Sequence Diagrams

Proceedings of 2020 Working Conference on Software Visualization (VISSOFT), 2020, 2020

Taher A. Ghaleb, Khalid Aljasser, Musab A. Alturki

On Security Analysis of Periodic Systems: Expressiveness and Complexity

Proceedings of the 7th International Conference on Information Systems Security and Privacy, ICISSP 2021, 2021

Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich, Vivek Nigam, Andre Scedrov and Carolyn Talcott

Resource and timing aspects of security protocols

Journal of Computer Security, 2021

Abraão Aires Urquiza, Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich, Vivek Nigam, Andre Scedrov and Carolyn Talcott

An Extensible Compiler for Implementing Software Design Patterns as Concise Language Constructs

International Journal of Software Engineering and Knowledge Engineering, 2021

Taher A. Ghaleb, Khalid Aljasser, Musab A. Alturki

Musab A. Alturki, PhD

Sitemap

Pages

Posts

projects

publications

talks

teaching