Add CBMC proof for s2n_stuffer_printf

[lrstewart]

Resolved issues:

Resolves #4298 (comment)

Description of changes:

Add a proof for the new s2n_stuffer_printf method.

I also changed the existing s2n_stuffer_wipe_n behavior and rewrote the associated proof. My s2n_stuffer_printf tracked the tainted flag closely and found some unexpected behavior in how s2n_stuffer_wipe_n handled the tainted flag. Previously, if s2n_stuffer_wipe_n resulted in wiping the last few bytes of a stuffer, the stuffer was also wiped-- specifically, the high_water_mark and tainted fields. This makes s2n_stuffer_wipe_n hard to reason about, and seems like a potential way to accidentally "untaint" a stuffer. wipe_n is about wiping individual bytes, not wiping the whole stuffer. I don't know why you'd have an outstanding raw pointer to a stuffer with write_cursor==0, but the memory still exists so you could, and it doesn't seem any different from having an outstanding raw pointer to wiped memory with write_cursor>0.

Testing:

Proofs pass.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.

[camshaft]

Thanks for doing this!

[feliperodri]

These updates are great! I'm quite happy to see such improvements over the CBMC harnesses. I only have a few remarks. First, I got this list of warning from the CBMC HTML report:

 Warnings

Functions omitted from test (unexpected):

    madvise
    s2n_blob_slice
    s2n_stuffer_wipe
    vsnprintf

Are these expected?

[feliperodri]

The function madvise is reachable in these harness, so I recommend you to include the stub we created for it. You only need to include it in your Makefile.

PROOF_SOURCES += $(PROOF_STUB)/madvise.c

[lrstewart]

These updates are great! I'm quite happy to see such improvements over the CBMC harnesses. I only have a few remarks. First, I got this list of warning from the CBMC HTML report:

 Warnings

Functions omitted from test (unexpected):

    madvise
    s2n_blob_slice
    s2n_stuffer_wipe
    vsnprintf

Are these expected?

You called out how to fix madvise in your other comment, and I fixed that. I thought I was handling s2n_blob_slice and s2n_stuffer_wipe by using REMOVE_BODY, but I guess not so I removed that. They're never hit because the stuffer never shrinks.

vsnprintf is the only one on the list now, and I think that's expected. We could stub it, but idk what we'd do other than the current default "assume it could return anything" behavior.