<div class="csl-bib-body">
<div class="csl-entry">Dong, N., Guanciale, R., & Dam, M. (2021). Refinement-Based Verification of Device-to-Device Information Flow. In <i>Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021</i> (pp. 123–132). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_21</div>
</div>
I/O devices are the critical components that allow a
computing system to communicate with the external environment.
From the perspective of a device, interactions can be divided
into two parts, with the processor (mainly memory operations
by the driver) and through the communication medium with
external devices. In this paper, we present an abstract model of
I/O devices and their drivers to describe the expected results
of their execution, where the communication between devices
is made explicit and the device-to-device information flow is
analyzed. In order to handle general I/O functionalities, both
half-duplex (transmission and reception) and full-duplex (sending
and receiving simultaneously) data transmissions are considered.
We propose a refinement-based approach that concretizes a
correct-by-construction abstract model into an actual hardware
device and its driver. As an example, we formalize the Serial
Peripheral Interface (SPI) with a driver. In the HOL4 interactive
theorem prover, we verified the refinement between these models
by establishing a weak bisimulation. We show how this result can
be used to establish both functional correctness and information
flow security for both single devices and when devices are
connected in an end-to-end fashion.
en
dc.language.iso
en
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
formal verification
en
dc.subject
refinement
en
dc.subject
serial interface
en
dc.subject
device driver
en
dc.subject
interactive theorem prover
en
dc.subject
information flow
en
dc.title
Refinement-Based Verification of Device-to-Device Information Flow
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.identifier.doi
10.34727/2021/isbn.978-3-85448-046-4_21
-
dc.contributor.affiliation
KTH Royal Institute of Technology Stockholm, Schweden
-
dc.contributor.affiliation
KTH Royal Institute of Technology Stockholm, Schweden
-
dc.contributor.affiliation
KTH Royal Institute of Technology Stockholm, Schweden
-
dc.relation.isbn
978-3-85448-046-4
-
dc.relation.doi
10.34727/2021/isbn.978-3-85448-046-4
-
dc.description.volume
2
-
dc.description.startpage
123
-
dc.description.endpage
132
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
2708-7824
-
tuw.booktitle
Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021
-
tuw.peerreviewed
true
-
tuw.relation.haspart
10.34727/2021/isbn.978-3-85448-046-4
-
tuw.relation.publisher
TU Wien Academic Press
-
tuw.relation.publisherplace
Wien
-
tuw.book.chapter
21
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
dc.description.numberOfPages
10
-
tuw.relation.ispartoftuwseries
Conference Series: Formal Methods in Computer-Aided Design
-
tuw.author.orcid
0000-0002-0629-4439
-
tuw.author.orcid
0000-0002-8069-6495
-
tuw.author.orcid
0000-0001-5432-6442
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
item.openaccessfulltext
Open Access
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.grantfulltext
open
-
item.mimetype
application/pdf
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
item.fulltext
with Fulltext
-
item.cerifentitytype
Publications
-
crisitem.author.dept
KTH Royal Institute of Technology Stockholm, Schweden
-
crisitem.author.dept
KTH Royal Institute of Technology Stockholm, Schweden
-
crisitem.author.dept
KTH Royal Institute of Technology Stockholm, Schweden