Re: [Edm] Tracking (and distinguishing) formal analysis

[Christopher Wood <[e-mail]>]

I agree that it’s useful for drafts to cite this work, but we should also acknowledge that analyses change over time. Sometimes there are bugs in the proofs or models. Sometimes new results emerge that complement or otherwise impact existing analyses. The unfortunate consequence of immutable RFCs is that we don’t have a good way to track these things. Adding them to the datatracker seems like a low effort workaround. 

Best,

Chris 

On Mar 15, 2023, at 9:13 AM, Lucas Pardue <[e-mail]> wrote:



To echo some of what Martin said, in the QUIC sphere I tend to see research in papers or proceedings. Some of that research has identified issues with a specific implementation, confirmed that the protocol behaves in deployments as intended, etc etc. While not strict formal verification, there is perhaps merit in collecting links to artefacts to help track _use and deployment_ of a protocol after the initial design work was done and the RFC cut.

Tangent: more of a tools discuss item probably - but having the list managed directly in the datatracker isn't the most user-friendly thing. As the number of items grows, it makes change management a bit tedious. It's also not clear to me who has write access (I assume just chairs and ADs?). A model where folks could propose their additions for review and approval would help crowd source that slightly. Currently as a non-logged in user, its not even obvious that the "Additional resources" field is such a free-form field and that we'd likely welcome people volunteering their own links there.

Cheers,

Lucas

On Wed, Mar 15, 2023 at 11:24 AM Martin Thomson <[e-mail]> wrote:

I tend to think that the draft should be citing work like what you reference.

Still, having references to implementations, analyses, or other relevant material, can still be valuable to collect the way you describe.  I think that this could help.  Given that this is a bag of tagged URLs, the bar for adding new types should be pretty low.

On that thought, I'd be OK with "explanatory blog posting" meeting the bar, as well, if you like.  We've had a ton of really good ones published over time for IETF work.  Sometimes they are the best way to get introductory-level background on the work.  Add those too.

(Tracking clicks might only offer the most vague approximation of "value".  Discussion might be a better indicator. Though in this case, the number of people qualified to read and contribute to that work is very much limited.)

On Wed, Mar 15, 2023, at 22:04, Christopher Wood wrote:
> Hi folks,
>
> One of the helpful contributions of this group was changes to the
> datatracker that help track implementations of specifications (under
> "additional resources"). I've used this for a couple of specifications
> [0], and I hope others find them useful [1].
>
> Implementations are not the only artifact that help with the
> development of specifications, though. Artifacts produced through
> formal analysis, such as executable models using tools like ProVerif or
> Tamarin and even pen-and-paper analyses, both change as the
> specification changes. As we develop specifications, new analyses
> appear over time, including after the final RFC is published.
>
> Given that these artifacts have similar churn as implementations, and
> complement specifications in a similar way as well, I'm wondering if we
> ought to extend the available tags in the datatracker to keep track of
> these things. As a strawman proposal, what do folks think about adding
> a "related_analyses" tag (similar to the "related_implementations" tag)
> to the set of available tags in the datatracker? We might use it like
> so:
>
>     related_analyses https://github.com/cloudflare/ohttp-analysis" rel="noreferrer nofollow" target="_blank">https://github.com/cloudflare/ohttp-analysis
> (Tamarin model of Oblivious HTTP)
>   
> Additionally, I'm wondering if we could also add a way to "flag"
> different resources so that they are easier to identify. Not everyone
> might know what a "Tamarin model" is. So for example, perhaps we could
> have colored label that says "analysis" (or something) next to the
> rendered item in the datatracker.
>
> Good idea? Bad idea? I'm curious to hear your thoughts. If interested,
> maybe we could discuss this in 116?
>
> Best,
> Chris
>
> [0] https://datatracker.ietf.org/doc/draft-ietf-ohai-ohttp/" rel="noreferrer nofollow" target="_blank">https://datatracker.ietf.org/doc/draft-ietf-ohai-ohttp/ as one
> example
> [1] I don't know how useful these are to others. Do we have a way to
> determine how many times these links are clicked?
> --
> Edm mailing list
> [e-mail]
> https://www.iab.org/mailman/listinfo/edm" rel="noreferrer nofollow" target="_blank">https://www.iab.org/mailman/listinfo/edm

--
Edm mailing list
[e-mail]
https://www.iab.org/mailman/listinfo/edm" rel="noreferrer nofollow" target="_blank">https://www.iab.org/mailman/listinfo/edm

--
Edm mailing list
[e-mail]
https://www.iab.org/mailman/listinfo/edm