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



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



On 11 May 2020, at 22:27, Abhishek Anand <abhishek.anand.iitg at gmail.com<mailto:abhishek.anand.iitg at gmail.com>> wrote:

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/



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.