coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Formally verified logging libraries?

From: Talia Ringer <tringer AT cs.washington.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Formally verified logging libraries?
Date: Fri, 17 Dec 2021 10:48:10 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=Pass smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mx6.cs.washington.edu
Ironport-data: A9a23:sLEJT64/0o3b4l9voS7y4QxRtIHFchMFZxGqfqrLsXjdYENS0TUByzdOUT+PbP2Kambwc9snYI3kp04AsMDXzoUwHAod+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t63yUjRxRSwNZie0SiyFb/6x/RGQ6YnSHuClUbSdZXgoLeNZYH5JZSxLy7ZRbrFA2oDR7zOl4bsekuWHULOX82Yc3lE8t8pvnChSUMHa41v0iLCRicdj5zcyn1FNZH4WyDrYw3HQGuG4FcbiLwrPIS3Qw4/Xw/stIovNfrfTd11UBLXJexeHkXpXXae+hR4EqyAvuko5HKNGOQEN02XPw483lYwlWZ+YEW/FOoXQguUbXBRCOyple7JP47/GJ3ejtsrVwkHbG5fp66k2URBuZuX0/c4qWD8eq6dwxCo2RhuEnqe9xK+xYvJ9g9wqasjtJoIW/H96pQw1p95OrYvrRrWUo9RDmig5ncBPG/nCYMxfZDZyBCksqiZnYj8/YK/SVs/x7pU+T9FZlL5Rja8nvS7Y10pu2aPtMdzaZtuMA8hZgy50Y0quE3vRWnkn2B63kFJpMU5AQsfEhmXkUZkSFbu36vlsxlCf2wT/zTUIAECjr6DRZlGWArpixo99xsbqhaMpslOiVdn8WRKkp3jCsxIBMzaVO4XW9ynVopfpD82l6qTog9KPhBHKdCP7eNDy6mK0og==
Ironport-hdrordr: A9a23:6pHtmKi6hIJBufXMkLLeAiqOR3BQXsUji2hC6mlwRA09TyXqraCTdZMgpH3JYVcqKRIdcL+7UpVoLUmyyXcX2+Qs1NWZNzUO0VHARL2KhrGN/9SPIUzDH6JmuZtdTw==
Ironport-phdr: A9a23:R5TFWhNodx2izGWIUIkl6nb+DRdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDv6wr3QKCBN+Bo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9AdgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6v95HJZwhFhDWxba5sIBmosA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo6ycZEAD+4APelCsoLzu1oOrR2xBQayHuPk1zhFhmPs3a071eQhHh/J3BY7Et0Sq3TYttv0O70JUeC1zanIyzrDb+9R2Tf78oTHbA0uoeyVUL92bMHexlUhGRnfgVWMtYzqISmV1uIVvmWU8+ZtUeyihWEppQ9/pjWj2tkgh5TVi4wa11zJ8Th0zoYoKdC3VkN2bsKpHZVfuiyYOYZ7Q8AvTnx1tCs4y7ALv4OwcisSyJk/2hLTdf+Kf5KW7h7/V+udOzh1iXB/dL+/mhq+6VasxvH4W8Wu01tHrjBJnsTNu30MzRDf98qKR/l780y8wziAzRrT5ftBIU0slarUNZohwrkom5oWvkXOHzX6l1ntjKOMeEQr4POo6+TmYrXgqZ+cK4h0igfkPqswh8O/HPw0MgkIX2eF5eSxzKDv8VP6TblQkPE6jqrUvIrVKMkZvKK0AxJZ3p4m6xmlDjem1NoYnWMALFJAYB+Hk5LpO1DIIPD3E/i/mU+hnytwx/zcMLzuGI7NLnjCkLfncrZ990lcyAwpwd9B+p1UF6kNIOjvVU/pqNzYEhg5PhSozObgEdVxz58RWWaSAqCCK67Sql+J5uc3I+aWfoMVuTD9K+Ik5/H0l3M5l0UdLuGV2s4cb2n9FfB7KW2YZ2Dti5EPCzQkpA07GdDjjFyLGQRSYXm/Repo+is6Do2rF6/IXcayiaeB3SG0AppQIG1KFwbfQj/Ta4yYVqJUO2qpKch7n2lcPVBOY4Q6kw6nrw/7zbV7KeyS9yEF58uLPD1d7PaVihgp9T1yANia1SeAQ3wmxgvgphczzP45qlc71V6Y0al+jOBfE5pe6+4bCm8H

Hi all,

I've been paying a lot of attention to these log4j vulnerabilities, and at this point there have been 3 consecutive releases all fixing vulnerabilities found in the previous ones. That made me wonder if anyone has ever built a formally verified secure logging library, especially with sufficiently interesting functionality. It has some of the properties that make verification super desirable:

- core infrastructure used by many dependencies

- security vulnerabilities have catastrophic consequences

but then it has some properties that make it difficult:

- it is entirely about I/O

- specifying correctness involves reasoning about complex interactions with the environment

Anyways, I don't really have ideas, but I'm curious if anyone else has thought about it at all, or implemented this, or has ideas. This isn't like a "I think this would solve everyone's problems" kind of thing, so much as a "I think this would be fun, interesting, and well motivated, but challenging enough that I wouldn't even be sure where to start" kind of thing.

Talia

[Coq-Club] Formally verified logging libraries?, Talia Ringer, 12/17/2021
- Re: [Coq-Club] Formally verified logging libraries?, John Sarracino, 12/17/2021