Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Concurrent Reactive Objects in Rust Secure by Construction
Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.ORCID-id: 0000-0002-1791-535x
Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
2019 (Engelska)Ingår i: Ada User Journal, ISSN 1381-6551, Vol. 40, nr 1Artikel i tidskrift (Refereegranskat) Published
Abstract [en]

Embedded systems of the IoT era face the software developer with requirements on a mix of resource efficiency, real-time, safety, and security properties. As of today, C/C++ programming dominates the mainstream of embedded development, which leaves ensuring system wide properties mainly at the hands of the programmer. We adopt a programming model and accompanying framework implementation that leverages on the memory model, type system, and zero-cost abstractions of the Rust language. Based on the outset of reactivity, a software developer models a system in terms of Concurrent Reactive Objects (CROs) hierarchically grouped into Concurrent Reactive Components (CRCs) with communication captured in terms of time constrained synchronous and asynchronous messages. The developer declaratively defines the system, from which a static system instance can be derived and analyzed. A system designed in the proposed CRC framework has the outstanding properties of efficient, memory safe, race-, and deadlock-free preemptive (single-core) execution with predictable real-time properties. In this paper, we further explore the Rust memory model and the CRC framework towards systems being secure by construction. In particular, we show that permissions granted can be freely delegated without any risk of leakage outside the intended set of components. Moreover, the model guarantees permissions to be authentic, i.e., neither manipulated nor faked. Finally, the model guarantees permissions to be temporal, i.e., never to outlive the granted authority. We believe and argue that these properties offer the fundamental primitives for building secure by construction applications and demonstrate its feasibility on a small case study, a wireless autonomous system based on an ARM Cortex M3 target.

Ort, förlag, år, upplaga, sidor
Ada Language UK Ltd. , 2019. Vol. 40, nr 1
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
Kommunikations- och beräkningssystem
Identifikatorer
URN: urn:nbn:se:ltu:diva-71246Scopus ID: 2-s2.0-85067078450OAI: oai:DiVA.org:ltu-71246DiVA, id: diva2:1256722
Anmärkning

Validerad;2019;Nivå 1;2019-04-09 (inah)

Tillgänglig från: 2018-10-17 Skapad: 2018-10-17 Senast uppdaterad: 2019-06-28Bibliografiskt granskad
Ingår i avhandling
1. !secure(system) <=?=> !safe(system): On Security and Safety of Industrial Software Systems
Öppna denna publikation i ny flik eller fönster >>!secure(system) <=?=> !safe(system): On Security and Safety of Industrial Software Systems
2019 (Engelska)Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
Abstract [en]

The focus of our research work is on readily accessible, embedded, real-time development with concurrency support. To this end, we develop the Real-Time For the Masses (RTFM) programming framework with a model of computation based on tasks and resources and that stipulates a timing semantics. Typically, hard real-time requirements are a characteristic of safety-critical applications. In contrast to runtime verification, such applications primarily require static assurances concerning safety and security attributes. This thesis discusses the building blocks for a statically analyzable programming paradigm for embedded real-time applications and its implementation. Svenska kraftnät funded the research presented in this thesis and set the scope to industrial automation. Consequently, we also investigate the applicability of our RTFM framework for scheduling and resource management for the runtime environments of industrial applications. We start by reviewing relevant and well-established industry standards to build background knowledge of the state-of-the-art safety and security requirements in software development. Special attention is placed on the IEC 61131 and IEC 61499 standards for industrial software development and their programming and execution model. We show the feasibility of using IEC 61499 as a holistic, distributed, and hierarchical model with mappings from the functional layer (IEC 61499 function block networks) and safety layer (PLCopen safety function blocks) to RTFM. We also demonstrate that our Rust-based RTFM implementation enables static verification for a myriad of safety and security attributes. Moreover, our investigations reveal a mutual dependency of safety and security in the context of software systems. For this reason, we believe and argue that safety and security cannot be considered independent during the design and implementation of safety-critical applications. Upon closer examination, we even conclude that safety and security are equivalent.

 

Ort, förlag, år, upplaga, sidor
Luleå: Luleå University of Technology, 2019
Serie
Doctoral thesis / Luleå University of Technology 1 jan 1997 → …, ISSN 1402-1544
Nyckelord
embedded systems, hard real-time, concurrency, model of computation, safety-critical, safety, security, industrial automation, RTFM, real-time for the masses
Nationell ämneskategori
Inbäddad systemteknik
Forskningsämne
Inbyggda system
Identifikatorer
urn:nbn:se:ltu:diva-73059 (URN)978-91-7790-320-8 (ISBN)978-91-7790-321-5 (ISBN)
Disputation
2019-05-08, A3024, Luleå, 13:00 (Engelska)
Opponent
Handledare
Tillgänglig från: 2019-03-01 Skapad: 2019-02-27 Senast uppdaterad: 2019-09-26Bibliografiskt granskad

Open Access i DiVA

fulltext(291 kB)50 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 291 kBChecksumma SHA-512
23dbcf70a2836f164b4a6aa861a05f29e837a7c96bf97b1912c2ce1eaf323752e777a389267813ec28e3e46ba2b92be22caaa64bb83d7888ddafaa97539b39d9
Typ fulltextMimetyp application/pdf

Scopus

Personposter BETA

Lindner, MarcusLindgren, Per

Sök vidare i DiVA

Av författaren/redaktören
Lindner, MarcusAparicio, JorgeLindgren, Per
Av organisationen
Datavetenskap
I samma tidskrift
Ada User Journal
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 50 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

urn-nbn

Altmetricpoäng

urn-nbn
Totalt: 239 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf