coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] formal models of peripheral devices like GIC, NIC

From: "Fernandez, Matthew" <matthew.fernandez AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] formal models of peripheral devices like GIC, NIC
Date: Mon, 11 May 2020 21:05:42 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=intel.com; dmarc=pass action=none header.from=intel.com; dkim=pass header.d=intel.com; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=0oaZrMcA+MmaqZU/BvM/6Ty5RrkatNHK3WtGto+20UU=; b=hBU2XIRFj4yhvcfHaMUY+kB4WqPVs71lqGdkDyKjC5Zlis4FkHr5Sf03qKVzBX7IH6G150lixQfxGrDM/+embLG+k+XCZKLXVIlsjWXH67BL9YlgJANIQELzIjIyS04hOx2e7PcN/pfNUtm1XF89ViQv+PNKXJmREj2GQreQx3W3Fuo/fhjBkv2daccvn3vFrtg3fFQOBDlRzm0KWQg7KryYiGYwAR/I9TNxXY4tM993acuUyJrwNHHGIr6qK5xD+gguM7QQSkPIL0cFbUosKN1f+9szd3RssR11zxShITpSGOr4EsBBjr+5BIhAoy2kqYPpIUqXLPRJI+sVU+RHlA==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=iw1F6LlRA22Yzj+Vii3kDtHUG6GmHC9ODSjMFGWAnMyLIarUwJtoFq5bgUBTeHuzHgVD/FYZ6MC2lb+CyfsBdzXsOdcKzqTmFqFGpZYumnlED3ilRO0g+8dRFefgiSVGNTB8azcMkBw0JO8psW7ksi4DiGWzj8eIU1MfeC74leUi1IPkRbSv8eLAW+MwhHsNhQX8g+dBZp7twqrAo/O7gUCg1wfWPv1oQFRxzxsU4FF7MXAhiE3ejg75fULq3khyLiOxCKsqoDOhdJoOoV8J1wavJYzOcSRwkhGEyeCq+aTsBa2sK96PiJAxq0O8lfUQGcFO7GIeYEXeYqQAQ39Vew==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=matthew.fernandez AT intel.com; spf=Pass smtp.mailfrom=matthew.fernandez AT intel.com; spf=None smtp.helo=postmaster AT mga09.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.2.0.6
Ironport-phdr: 9a23:v5KH0BeDz5YTdzqFmWk6HGsflGMj4u6mDksu8pMizoh2WeGdxc26ZBSN2/xhgRfzUJnB7Loc0qyK6v2mCDRLuMrR+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi2oAnLssQanYRuJrs+xxbKv3BFZ/lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/WfKgcJyka1bugqsqRxhzYDJfIGbOvlwfq3fctMbWWVOUd1cWDZdDo+gdYYDE/YNMOReooLgp1UOtxy+BQy0Ce/hyjFHmGX23asg3OQnDA7Jwg0hE8oTu3rTttr1KLsSUeCrw6jGwznIcvRb2TLn54jUbhAhoe+DXLxqfcrf10YvDQXFgU+WqYP4ITyU1/8As2md7+p8S+2vj3QrpB12ojiq38ohjJTCiY0JxF7e7yp53Jo1KsOiSE59edOpFJRduSGHO4ZoXM8vXmFmtTomxrAGuJO2fCkHxZonyhLDavGKcIaG7xHgWeuNPDt1gG5odb2jihi8/katxOPxW8+p21hEqSpFl8PDtnEL1xHL5ciHS+d9/ke82TmUzQzc9uZEIUUsmaXHLJ4h2LgwmYQXsUTHBCP5hlj5jLKQe045+eao8/zqbqjoq5KTLYN4lw/zP6s0lsCiD+k1MxICU3aU9Oik1rDu81f1TKtKg/Esj6XUs5HXKd4FqqO2HQNZypgv5hejAzqo1dkUgGULI0lEdR+CkYTlJ1LDLfXmAfq+jVShlTJmy+3aMrDnH57DNGLMkK37crZ480NcyBQ8zdRY559MD7EBL+j8VlP1udDCDx85NRC0zPjjCNlnyoweXmePDreYMKPUr1CI+voiL/SCaYIaojrxNvYo6vH0gXMkl1IQfLOl0YUYZXygG/RpOUSZYX7igtcbFmcKuxIzTOnwh12eTT5TZ2i9Xqwm6jE1Fo2mF4HDSZqrgLOcwii6H4ZbZmFAClCQD3joc5+IVOsLaCKXOsNhiCALVaC9S4890hGjrBP1y71+LubN5iIYsY/j28Nu6u3IlRAy8CR0AN6H32GMSWF0hGIISCUs0KBxu0wugmuEhOJzhOUdHthO7dtIVB07PNjS1aYyX9v1Q0fKesqDYFegWNSvRz8rGIEf2dgLNgxTFs+khxbP0jjuS5oci6CLCYN+uvbZ1mTtJ8tijXjLzq8oiVUrUONOM3Grguh08A2FVN2BqFmQi6v/LfdU5yXK7mrWlTPT7nEdaxZ5VOD+ZV5aZkbSqo2mtEbNRuf/T7UhLgZFj8WFL/kSM4G7vRB9XP7mfe/mTSepgW7pXESJwK+BaMzhfGBPhHyMWnhBqBga+DO9DSZ7Ay6gp2zECzk3TADuZV/h9a91r3bpF0I=
Ironport-sdr: AlK9VShszggd4PyAHlh3OyPoc2/5+xwiylat5r0CYLGzqAgglcjRj5KM7ZnEhUSWHlEsqfyHNe Cly0tubvNpdg==
Ironport-sdr: gntZj47W7cNRTW7AzVTmOE7pgBfM1EO5J+sTT9JahG0pIWXoZjZsBzLX5soGI5GSMXnqUpeE62 XQ/EfBjemqxQ==

There’s a partial model of the GIC in the seL4 proofs [0]. It only contains the bare minimum that was necessary for their proofs, but maybe this is a good jumping off point.

[0]: https://github.com/seL4/l4v

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> On Behalf Of Abhishek Anand
Sent: Monday, May 11, 2020 13:27
To: coq-club <coq-club AT inria.fr>; cl-isabelle-users AT lists.cam.ac.uk
Subject: [Coq-Club] formal models of peripheral devices like GIC, NIC

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/

[Coq-Club] formal models of peripheral devices like GIC, NIC, Abhishek Anand, 05/11/2020
- RE: [Coq-Club] formal models of peripheral devices like GIC, NIC, Fernandez, Matthew, 05/11/2020
  - Re: [Coq-Club] formal models of peripheral devices like GIC, NIC, Larry Lee, 05/11/2020
- Re: [Coq-Club] [isabelle] formal models of peripheral devices like GIC, NIC, Hira Taqdees Syeda, 05/12/2020