coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Formally verified logging libraries?

From: John Sarracino <jsarracino AT cornell.edu>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Formally verified logging libraries?
Date: Fri, 17 Dec 2021 13:42:55 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=cornell.edu; dmarc=pass action=none header.from=cornell.edu; dkim=pass header.d=cornell.edu; 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-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=2C0iCqQqPtfdXjjYzgjUkO2JBS6hl+cdxOsLyxUTCNo=; b=PlXLiPkHJIA5RK6xbTYPvjJ+L9cgtgWsr6SytUBloLnoNSd/k25lLiKqxdpNLyUIyfYCjhvh4Ey9UJuyr225gkkKfZ3KmXl6pJIuQzEN2tVRCzBm80k+bgPZnUqYO+NdFPgEdBWO+hVVCtfMO+c743bv0122XWl1lQoJvuuIhVH82RkLVj1bgfT0bQ11Prif+Lq8ZIJN73g76bjLpX2jlIteSevl9uvxyUZ9bAeEfc0coioMc1ARncMaTqlYRA8ufVj050b69Johs0kkECEt7mdxz2TYA3kAoon2XDZJoVEW8sQTk+rUg1bNZBg/kGeqIaeBpJBODtgKLFm/KSOL6Q==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=EERQJ2VGtVEpnAVYS3wArIiKZl67ci98iAB2N4EM0rOF0xQNe+bFgoMQ8YVUV/VYGWdCNmgSIdV5pVtZBxcW7N1uItnDF8qlVkrihpB2ailYuP5ph99xw2dCGiUS4a3D7BiyOB+Us/d0Bqx06dM4vicEml8RmYHZ2ke/WzLsfsAAChYr7b2DpRS3QVuIcoqcd/GiaFPQ1wpkxnrj+D1321s3dKeKL77KGPheI+mqMzGWbZReyXtqahpd0I/VRDA0VZamm2Q4WmueKzvr4HxpvWtMRo+Qz9bZUc+PxPcupjhrwYbyfVxixHLlXZqUQJS+Wr2xyDUCCAEqz6XljClQ/w==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jsarracino AT cornell.edu; spf=Pass smtp.mailfrom=jsarracino AT cornell.edu; spf=Pass smtp.helo=postmaster AT NAM12-MW2-obe.outbound.protection.outlook.com
Ironport-data: A9a23:v7l+FahDs3UIi3E08d1GScRuX161XBEKZh0ujC45NGQNrF6WrkUAyGseXG6AP/uDNzT9fttxbd6/9ksEuZSGz9QwQAM5+VhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t51GAjX4wXFdokb0/n9BCZC86yksvU20buCkUredYHkuHVYMpBoJ0HqPpcZp2uaEvvDiW2thifuqyyHuEAfNNwxcagr42IrfwP9bh8kejRtD1rAIiV+ni3eF/5UdJMp3yahctBIUSKEMdgKxb76rIL1UYgrkExkR5tONyt4Xc2Usa5uLZ02rtSATXKKvxB9fuiY1z6A3cuIGbltagCmImNY3z8hRsZu3SkEiOaikdOY1D0EeSnkhe/capPmeeSXXXc+7lyUqd1Pu2Px0Fkg9PIsf0u1wG2dD8fheJTwQBvyGr7vvne3lFLI07igkBJKyZ9hA0p169hnSCu9jSpTeSY3R9NpA1XExgNpPFLDQfaIkhZBHeEyVOFsSLg5CUNRmiL393j+lLmMGvAnA/exq9zeG5RJV+73LHNrxW9Wsed9zih/A8z+CpHCR7goyMdWezX+A7Siqj+qWxyT9AttKSfu/6+Jgh0CVyioLEhoKWFCnoP6/zEmjR9ZYLE9S8S0rxZXePXeDFrHVNyBUalbd53bwmua8EtHWLCmr44+NuUO8OTJBSTRMLts7qMUxWDomkEeTmM/kDiBut7vTTm+B8rCTrnW5Pi19waoqe3ofVQVcizX8iNhbs/4NZo8L/G2JYhndEjbqxT2OqG4zi6h7YQsjyfCg5V6e696zjsGhc+P2jzk7mkqu6Rl/aYqhIYGk9DA3KN4owJmxFjG8gZTPpyRSAC3iw31AeOxhjdjhxI2U2ss=
Ironport-hdrordr: A9a23:w9r116NNETf3CcBcT07155DYdb4zR+YMi2TDiHoddfUFSKalfp6V98jzjSWE8Ar5K0tQ4uxoWZPwCk80kKQY3WB/B8bHYOCLggqVxcRZnPLfKl7bamfDH4xmpMBdmsFFYbWeY2SSz/yKhjVQeOxQo+VvhZrY4Ns2uE0dLz2CBZsB0y5JTiKgVmFmTghPApQ0ULCG4NBcmjamcXMLKuymG3gsRYH41pH2vaOjRSRDKw8s6QGIgz/twqX9CQKk0hAXVC4K6as+8FLCjxfy6syYwr6GI17npiHuBqZt6ZvcI+h4dY+xYw8uW3fRYzOTFcVcsnu5zXUISa+UmRIXeZL30m0d1oxImg7slyeO0FbQMkDboUoTwm6nxlmCjXT5p8vlADo8FspanIpcNgDU8kw6obhHodR2Nk+ixu5q5Cn77VPADhnzJmFXv1vxpWBnnf8YjnRZX4dbYLhNrZYH9EcQFJsbBir15I0uDeErVajnlb5rWELfa2qcsnhkwdSqUHh2FhCaQlIassjQ1zRNhnh2w0YR2cRalHYd85A2TYVC+o3/Q+1VvaALStVTYbN2Be8HT8fyAmvRQQjUOGbXOljjHLFvAQO5l3c22sRG2AiHQu138HICouWzbLoDjx9MR6vHM7z+4KF2
Ironport-phdr: A9a23:WtkZ4hMzM4juALSIDu8l6nZBChdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDv6wr3QKCBN+Ho9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9AdgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6v95HJZwhFhDWxba5sIBi5sA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT4n/m/Klsx+gqFVoByjqBNjzIHZe5uaOOZ7fq7HYd8WWWhMU8BMXCJBGIO8aI4PAvIFM+Zfr4n9oUYFowakCgm2HuPg0CNHhn7w3a09zu8sFgPG3Bc6ENIUqnTbtsn6NKYUUeCy16TH0TLDb+lQ2Tjj7IjIdgotru+RUrJtaMfcz1QkGAzZgFuKs4PlIy+V2foXs2id9+dtV/+ihmoppQxsrDWixdkhh5XHiI4I1l3J9iV0zZsxKNC3RkB2Yd6qHIVOuy+VK4Z6XsMvTW91tSs61rELu5+2cS4Xw5opwB7fbuaIc4mO4h/7SOaQLzZ4hG55eL2hnRa+61Svyur5VsSyzV1ErTJFn8HDu3wRzRDf99SLR/ln8ku/1juC2Brf5vxYLU00jabXNZ8szqI+m5cWrEjPAjT5lUTzgaCMakkp9O2l5/r6brr9o5KRMpJ4hwL4P68zgMKwG/44PRILX2WD+eSzyrnj/UrhTbtSkvA4lbTVvI7DKcocpqG1HRZZ0oE45BmhFTum18kYnWUcI1JCZRKHiZXmN0vWIPDiCve/n0qjnyt3x/DHOb3hBI/BLn/ekLf9ebZ97ElcyAkpwd9D4JJUD6kNIPP1WkDvqNzVFhA0PxCuz+r6FNlw1JkSVXyAD6KWKq/erEOE6+I3L+mJfoAVuTL9K/Y/5/7piH80gV0dfbKz0psNcnC3BOhpI0SfYXrrmdoODWAKvhA4TOP0jF2CVSRfaGivUKIh/j07Ep6pDZ/fRoCxh7yMxDu0HppPZmxfFl+MFWroeJ6fVvcXaCOSJ9dhnSYeWbigTY8hzxCuuxXgx7ppNOqHshEf4Njo08Ew7OnOnzkz8yZ1BoKTySvFG2pzhyYDQyI89KF5u010jFmZh/tWmftdQP5U5/UBaQ4gL5fXzup9Q4TwQQvbZN6CSVChat6hGzc8StZ3ztMTNRUuU+6+hwzOinL5S4QekKaGUcRcGkf01H/rIct5zzDL2LRz1zHOreNEMnegi6p7sQXfGtyQ+614v4CDUP1GmQvyriKEx2fIu1xEWgltV6mDRWoYekbdsdX+4AXFUqOqDrMkdABGzJzbQpY=

Hi Talia,

I’ve been thinking about this as well, and I also don’t have much of a concrete proposal. My understanding is that in the latest patch 2.16.0, log4j gave up and just completely disables the problematic I/O (JNDI interpolation). I don’t know how widely used this feature is, but, I’ll bet that it’s important and popular.

It would be interesting IMO to formalize secure logging as a mix of information-flow control with I/O primitives, e.g., the external data is untrusted/low and JNDI lookup functions are trusted/high.

Then, the trick would be to ensure that endorsement/filter functions are correctly applied, and you could imagine a rich foundational logic for this. For example one spec is that all JNDI LDAP arguments are prefixed by localhost, and then you have to show that the filtering logic actually does ensure this property. This might seem like a trivial proof but it has already lead to a vulnerability in one of the mitigations: https://twitter.com/marcioalm/status/1471740771581652995

Cheers,

John

On Dec 17, 2021, at 5:48 AM, Talia Ringer <tringer AT cs.washington.edu> wrote:

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