Concurrent Reactive Objects in Rust Secure by Construction

↓ Direkt till sidans innehåll
↓ Direkt till sidans sekundära innehåll (sidomenyn)

Sökning: WFRF:(Lindnér Per) > (2015-2019) > Concurrent Reactive...

Lindner, MarcusLuleå tekniska universitet,Datavetenskap (författare)

Concurrent Reactive Objects in Rust Secure by Construction

Artikel/kapitelEngelska2019

Förlag, utgivningsår, omfång ...

Ada Language UK Ltd.2019
electronicrdacarrier

Nummerbeteckningar

LIBRIS-ID:oai:DiVA.org:ltu-71246
https://urn.kb.se/resolve?urn=urn:nbn:se:ltu:diva-71246URI

Kompletterande språkuppgifter

Språk:engelska
Sammanfattning på:engelska

Ingår i deldatabas

SwePubSwePub

Klassifikation

Ämneskategori:ref swepub-contenttype
Ämneskategori:art swepub-publicationtype

Anmärkningar

Validerad;2019;Nivå 1;2019-04-09 (inah)
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.

Ämnesord och genrebeteckningar

NATURVETENSKAP Data- och informationsvetenskap Datavetenskap hsv//swe
NATURAL SCIENCES Computer and Information Sciences Computer Sciences hsv//eng
Dependable Communication and Computation Systems
Kommunikations- och beräkningssystem

Biuppslag (personer, institutioner, konferenser, titlar ...)

Aparicio, JorgeLuleå tekniska universitet,Datavetenskap(Swepub:ltu)jorapa-7 (författare)
Lindgren, PerLuleå tekniska universitet,Datavetenskap(Swepub:ltu)pln (författare)
Luleå tekniska universitetDatavetenskap (creator_code:org_t)

Sammanhörande titlar

Ingår i:Ada User Journal: Ada Language UK Ltd.40:11381-6551

Internetlänk

Hitta via bibliotek

Ada User Journal (Sök värdpublikationen i LIBRIS)

Till lärosätets databas

Hitta mer i SwePub

Av författaren/redakt...: Lindner, Marcus; Aparicio, Jorge; Lindgren, Per

Om ämnet

NATURVETENSKAP: NATURVETENSKAP; och Data och informa ...; och Datavetenskap

Artiklar i publikationen: Ada User Journal

Av lärosätet: Luleå tekniska universitet

Sök utanför SwePub

Sök vidare i:: Google; Google Book Search; Google Scholar

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.

LIBRIS.kb.se