Generation of Formal Specifications for Smart Contracts from Architectural Specifications

Aus SDQ-Wiki
Wechseln zu: Navigation, Suche
Ausschreibung (Liste aller Ausschreibungen)
KASTEL-Logo 1000.png Typ Bachelorarbeit oder Masterarbeit
Aushang Generation of specifications for smartcontracts from architecture.pdf
Betreuer Wenden Sie sich bei Interesse oder Fragen bitte an:

Frederik Reiche (E-Mail:: frederik.reiche@kit.edu, Telefon:: +49-721-608-45992)

Motivation

Smart contracts are programs that run on a blockchain infrastructure. They take control over assets on that infrastructure and perform automated, deterministic execution of an agreement between network participants. Smart contracts are a prime target for security attacks, because they manage resources representing valuable assets. Due to their distributed nature, bugs are hard to fix which makes them susceptible to attacks exploiting programming errors. This makes rigorous formal analysis of smart contracts highly desirable. Security risks in smart contracts can also arise due to their distributed interaction and deployment. Capturing such characteristics on codelevel is difficult. Therefore architecture description languages like the Palladio Component Model (PCM) can be used to provide a more complete model of the system. To benefit from the architecture as well as the code, our goal is the usage of the PCM to create a precise model of a smart contract’s functionality and interaction to enable the generation of formal specifications on the source-code level.

Tasks

Your research is located on the connection between the architectural domain and the sourcecode and verification domain for blockchain and smart contracts including

  • Research about smart contract properties that can be described on architectural level
  • Extension of the Palladio Component Model for a selection of these properties
  • Automatic generation of formal specification

Benefits

  • Work on current technologies like model-driven engineering, blockchain and smart contracts
  • Research in the field of software security in the context of the ”Kompetenzzentrum für angewandte Sicherheitstechnologie“ (KASTEL)
  • Intensive supervision of your thesis and a good working climate