Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] formal models of peripheral devices like GIC, NIC

view this post on Zulip Email Gateway (Aug 23 2022 at 09:07):

From: Abhishek Anand <abhishek.anand.iitg@gmail.com>
Has someone built formal models of peripheral devices like Arm's Generic
Interrupt Controller (GIC), network interface cards that could be suitable
for proving correctness properties of software driving them (e.g. OS,
network driver)?
I'd be grateful for pointers to such work. The models need not be in
Coq/Isabelle, as long as there is a plausible way to convert them to
Coq/Isabelle models that describe the behavior of such devices.

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/

view this post on Zulip Email Gateway (Aug 23 2022 at 09:07):

From: Hira Taqdees Syeda <hira@chalmers.se>
Hi Abhishek,

Has someone built formal models of peripheral devices like Arm's Generic
Interrupt Controller (GIC), network interface cards that could be suitable
for proving correctness properties of software driving them (e.g. OS,
network driver)?

Not ARM’s peripheral devices, but I have, in my PhD, developed a formal model (in Isabelle/HOL) of
ARMv7-A translation lookaside buffer (TLB) based on the reference manual. I have then soundly
abstracted this model using data refinement to extract an abstract model that is easier to reason about
from software point of view. Using the abstract TLB+page tables as the memory model, I have
further developed a logic for reasoning about low-level programs in the presence of cached
address translation, and have with ease extracted invariants for user and kernel level code,
including context switch and page table manipulations.

Here are some links:

Publications:
in chronological order

  1. Reasoning about Translation Lookaside Buffers, LPAR17.
    https://easychair-www.easychair.org/publications/paper/gNH

  2. Program verification in the presence of cached address translation, ITP18
    https://link.springer.com/chapter/10.1007/978-3-319-94821-8_32

  3. Formal Reasoning Under Cached Address Translation, JAR20
    https://link.springer.com/article/10.1007/s10817-019-09539-7

PhD thesis:
https://unsworks.unsw.edu.au/fapi/datastream/unsworks:60079/SOURCE02?view=true

Ongoing work: to develop a formally verified TLB-aware compiler.

Isabelle Theories: https://github.com/SEL4PROJ/tlb

Hope this helps,
Thanks
Hira

Last updated: Nov 21 2024 at 12:39 UTC