[Verifpal] Verifpal 0.5

[Nadim Kobeissi]

Dear Loup,

Glad to see all the green lights — I feel like we have made excellent progress with the release of 0.5.
Did you notice also that the `_` feature was implemented? I remember that you asked for it.

Regarding your “USE()” idea, I wanted to ask you to please test using HASH instead and see if Verifpal produces output that conforms with your requirements. If so, then HASH should be sufficient. Please try it out and get back to me.

Unrelated: I really want to rename HMACVERIF to ASSERT, but am annoyed by how this will break backwards compatibility.

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On Sep 8, 2019, at 9:55 PM, Loup Vaillant David <loup at loup-vaillant.fr> wrote:
> 
> Excellent, thanks!
> 
> Just tested on my test files, and except for a false positive, it works
> as expected:
> 
> - ok.vp             : green light as expected.
> - unchecked_aead.vp : green light… as expected.
> - no_decryption.vp  : error is reported, this is perfect.
> - unguarded_alice.vp: authentication is broken, as expected.
> - unguarded_bob.vp  : confidentiality is broken, as expected.
> - hmac_ok.vp        : false positive: "confidentiality broken"
> 
> Now the next step, I think, would be to get rid of that false positive.
> I'm OK with false positives, *if* they're rare enough. But this is a
> fairly trivial model. I suspect we're hitting a fairly broad class of
> false positives here, not just narrow corner case. I believe this
> should be addressed before version 1.0.
> 
> ---
> 
> Regarding my uneasiness about giving a green light in unchecked_aead, I
> may have a solution. Failing to check a checked primitive means we
> don't block execution. But the primitive still fails to produce a
> meaningful value, protecting us against most attacker interference. The
> big problems arise when we actually use unauthenticated data for
> something significant, such as a decryption.
> 
> The thing is, the additional data will often not be used at all in the
> model. If for instance, it is something like an identifier the
> recipient can then check against a list of valid senders, Verifpal has
> no way of representing it —it's out of scope.
> 
> How about having a generic way to use a value, without telling Verifpal
> what that use is exactly?  Something like `USE(data)`. We could modify
> the last Bob in `ok.vp` thus:
> 
>    principal Bob[
>        ss_        = a_public^b
>        key_       = HASH(ss_)
>        plaintext_ = AEAD_DEC(key_, ciphertext, ad)?
>        _          = USE(ad)
>    ]
> 
> That way we clearly signal to Verifpal that we are relying on `ad` for
> some security sensitive matter, and that it'd better be authenticated,
> or be derived from authenticated values. In this case, removing the
> question mark should cause Verifpal to warn us about unauthenticated
> `ad` (as successfully used in the USE primitive).
> 
> (We could replace "USE" by "RELY_ON" or something.)
> 
> While we're at it, something similar could be done with plaintext_:
> 
>    principal Bob[
>        ss_        = a_public^b
>        key_       =
> HASH(ss_)
>        plaintext_ = AEAD_DEC(key_, ciphertext, ad)?
>        _ 
> = USE(ad)
>        _          = USE(plaintext_)
>    ]
> 
> The idea behind AEAD_DEC is that it should not produce a meaningful
> value if its internal checks fails. So, removing the question mark, and
> allow attacker interference should not cause `plaintext_` to be under
> attacker control. But real implementations often *do* produce some kind
> of `plaintext_`: an empty buffer, a buffer full of zeroes, or
> uninitialised memory (that last one is potentially nasty). If that
> broken plaintext is not used in the model itself, it might be a good
> idea to let the user mark it as used by the application itself.
> 
> Here, the additional error I would expect if we remove the question
> mark is that `plaintext_` is successfully used in `USE(plaintext_)`,
> but is garbage when `ciphertext` or `ad` is sent by the attacker.
> 
> Just a suggestion, though. There may be better alternatives.
> 
> Loup.
> 
> 
> 
> 
> On Sun, 2019-09-08 at 19:16 +0200, Nadim Kobeissi via Verifpal wrote:
>> Hello everyone,
>> Verifpal 0.5 is now available.
>> 
>> RELEASE NOTES
>>    - Increased analysis speeds by only mutating relevant values.
>>    - Fixed even more parsing errors pointed out by Mike.
>> Take note of the release notes for the previous version as well,
>> which were quite substantial:
>>    - NEW: nil keyword. Self-explanatory (by popular request).
>>    - NEW: _ can be used to assign anonymous constants (by popular
>> request).
>>    - Fix yet more parsing errors pointed out by Mike.
>>    - More fixes and improvements to authentication queries.
>>    - Added a new hopefully instructional example model:
>> ephemerals_and_signature.vp
>> 
>> INSTALLING AND UPDATING
>>    - If you’re fine with running arbitrary scripts in your terminal,
>> you can instantly update like this:
>>        - bash -c 'curl -sL https://verifpal.com/install|bash'
>>    - Or you can download a pre-compiled binary here:
>>        - https://source.symbolic.software/verifpal/verifpal/releases
>> 
>> NOTES ABOUT THIS VERSION
>>    - As usual, please continue your testing, everyone!
>> 
>> Looking forward to hearing from you all!
>> 
>> Nadim Kobeissi
>> Symbolic Software • https://symbolic.software
>> Sent from office
>> _______________________________________________
>> Verifpal mailing list
>> Verifpal at lists.symbolic.software
>> https://lists.symbolic.software/mailman/listinfo/verifpal
> <hmac_ok.vp>