Static Worst-Case Resource Analysis for Substrate Pallets

Simon Nicolas Perriard
2023
Projet étudiant

We present saft, the first attempt of a static analyzer that extracts the asymptotic function complexity for the Polkadot/Substrate ecosystem, where the burden of accounting for computation resource consumption is put on the developer. saft is a tool meant to be used in a complementary way with pre-existing development tools to improve the Substrate-based blockchain security. saft combines two techniques to analyze the MIR generated from the compilation of the blockchain subsystems, the pallets: (i ) abstract interpretation for the over-approximation of the concrete semantics and extraction of complexity asymptotics and (ii ) symbolic execution to track the length of dynamically sized vectors, increasing the precision of (i ). The developers can then compare saft output with their resource consumption computation. Our experimental evaluation showed that the tool scales well with arbitrary pallets, given some manual specifications.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (20)

Publications associées (33)

MOOCs associés (6)

Computational complexity

In computer science, the computational complexity or simply complexity of an algorithm is the amount of resources required to run it. Particular focus is given to computation time (generally measured by the number of needed elementary operations) and memory storage requirements. The complexity of a problem is the complexity of the best algorithms that allow solving the problem. The study of the complexity of explicitly given algorithms is called analysis of algorithms, while the study of the complexity of problems is called computational complexity theory.

Complexité en espace

En algorithmique, la complexité en espace est une mesure de l'espace utilisé par un algorithme, en fonction de propriétés de ses entrées. L'espace compte le nombre maximum de cases mémoire utilisées simultanément pendant un calcul. Par exemple le nombre de symboles qu'il faut conserver pour pouvoir continuer le calcul. Usuellement l'espace que l'on prend en compte lorsque l'on parle de l'espace nécessaire pour des entrées ayant des propriétés données est l'espace nécessaire le plus grand parmi ces entrées ; on parle de complexité en espace dans le pire cas.

Quantum complexity theory

Quantum complexity theory is the subfield of computational complexity theory that deals with complexity classes defined using quantum computers, a computational model based on quantum mechanics. It studies the hardness of computational problems in relation to these complexity classes, as well as the relationship between quantum complexity classes and classical (i.e., non-quantum) complexity classes. Two important quantum complexity classes are BQP and QMA.

Digital Signal Processing I

Basic signal processing concepts, Fourier analysis and filters. This module can be used as a starting point or a basic refresher in elementary DSP

Digital Signal Processing II

Adaptive signal processing, A/D and D/A. This module provides the basic tools for adaptive filtering and a solid mathematical framework for sampling and quantization

Digital Signal Processing III

Advanced topics: this module covers real-time audio processing (with examples on a hardware board), image processing and communication system design.

Latency Interfaces for Systems Code

Rishabh Ramesh Iyer

This thesis demonstrates that it is feasible for systems code to expose a latency interface that describes its latency and related side effects for all inputs, just like the code's semantic interface describes its functionality and related side effects.Sem ...

EPFL2023

We present a combination technique based on mixed differences of both spatial approximations and quadrature formulae for the stochastic variables to solve efficiently a class of Optimal Control Problems (OCPs) constrained by random partial differential equ ...

EPFL2022

FANOK: Knockoffs in Linear Time

Quentin Rebjock

We describe a series of algorithms that efficiently implement Gaussian model-X knockoffs to control the false discovery rate on large-scale feature selection problems. Identifying the knockoff distribution requires solving a large-scale semidefinite progra ...

SIAM PUBLICATIONS2021