The Coq mailing list

[Hira Taqdees Syeda <hira AT 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

On 11 May 2020, at 22:27, Abhishek Anand <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/