Opin vísindi

Developing theoretical foundations for runtime enforcement

Show simple item record

dc.contributor Háskólinn í Reykjavík
dc.contributor Reykjavik University
dc.contributor.advisor Luca Aceto, Anna Ingólfsdóttir, Adrian Francalanza
dc.contributor.author Cassar, Ian
dc.date.accessioned 2021-09-08T14:46:46Z
dc.date.available 2021-09-08T14:46:46Z
dc.date.issued 2021-01
dc.identifier.isbn 9789935953766
dc.identifier.isbn 9789935953773 (eISBN)
dc.identifier.uri https://hdl.handle.net/20.500.11815/2673
dc.description.abstract The ubiquitous reliance on software systems is increasing the need for ensuring their correctness. Runtime enforcement is a monitoring technique that uses moni- tors that can transform the actions of a system under scrutiny in order to alter its runtime behaviour and keep it in line with a correctness specification; these type of enforcement monitors are often called transducers. In runtime enforcement there is often no clear separation between the specification language describing the cor- rectness criteria that a system must satisfy, and the monitoring mechanism that actually ensures that these criteria are met. We thus aim to adopt a separation of concerns between the correctness specification describing what properties the sys- tem should satisfy, and the monitor describing how to enforce these properties. In this thesis we study the enforceability of the highly expressive branching time logic μHML, in a bid to identify a subset of this logic whose formulas can be adequately enforced by transducers at runtime. We conducted our study in relation to two different enforcement instrumentation settings, namely, a unidirectional setting that is simpler to understand and formalise but limited in the type of system actions it can transform at runtime, and a bidirectional one that, albeit being more complex, it allows transducers to effect and modify a wider set of system actions. During our investigation we define the behaviour of enforcement transducers and how they should be embedded with a system to achieve unidirectional and bidirectional enforcement. We also investigate what it means for a monitor to adequately enforce a logic formula, and define the necessary criteria that a monitor must satisfy in order to be adequate. Since enforcement monitors are highly intrusive, we also define a notion of optimality to use as a guide for identifying the least intrusive monitor that adequately enforces a formula. Using these enforcement definitions, we identify a μHML fragment that can be adequately enforced via enforcement transducers that drop the execution of certain actions. We then show that this fragment is maximally expressive, i.e., it is the largest subset that can be enforced via these type of enforcement monitors. We finally look into static alternatives to runtime enforcement and identify a static analysis technique that can also enforce the identified μHML fragment, but without requiring the system to execute.
dc.language.iso en
dc.rights info:eu-repo/semantics/openAccess
dc.subject Formal methods (Computer science)
dc.subject Monitoring
dc.subject Enforcement
dc.subject Logic in computer science
dc.subject Tölvunarfræði
dc.subject Hugbúnaður
dc.subject Tölvuöryggi
dc.subject Doktorsritgerðir
dc.title Developing theoretical foundations for runtime enforcement
dc.type info:eu-repo/semantics/doctoralThesis
dc.contributor.department Tölvunarfræðideild (HR)
dc.contributor.department School of Computer Science (RU)
dc.contributor.school Tæknisvið (HR)
dc.contributor.school School of Technology (RU)

Files in this item

This item appears in the following Collection(s)

Show simple item record