Unwind Issue: How to make a loop inductive? about cbmc HOT 46 OPEN

You might take a look at my "cbmc-examples" repository. This contains a selection of simple functions and their verification. All the examples use contracts (including loop invariants) to show how unbounded verification can be done with CBMC.

The "arrays" subdirectory there includes function that do array initialization, assignment, and some cryptographic things like constant-time equality and conditional copy.

See https://github.com/rod-chapman/cbmc-examples/

• Rod (AWS Cryptography)

from cbmc.

I'm not sure what the error itself means. Is it saying that we should only check invariant after the loop has started or we should not?

This error means the loop contracts are not inductive. Take your invariant __CPROVER_loop_invariant( i < cbData ) as an example. When one iteration starting with i equals to cbData-1 which satisfied the invariant, i will become cbData at the end of the iteration and break the invariant. I think the invariant for the loop should be i <= cbData.

To get a better idea of why some properties fail, you can run CBMC on the produced goto program with the flag --trace to see the playback of the failure.

from cbmc.

The loop invariant needs to be "i <= cbData", since the invariant is verified just before the loop exit condition gets evaluated. It's not exactly intuitive, but see my examples that I mentioned earlier.

from cbmc.

Here's MLKEM (aka "Kyber"): https://github.com/awslabs/LibMLKEM/tree/main/spark_ada
And here's the whole of NaCl: https://github.com/rod-chapman/SPARKNaCl
Language: Ada2012 (SPARK subset)
Toolset: SPARK Pro

from cbmc.

I'm also wondering about general approach to make loops inductive(what's possible and what's not with CBMC) and if there's any documentation on that.

from cbmc.

Yes, CBMC support loop contracts to prove loops inductively: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/contracts/doc/user/contracts-loop-invariants.md.
You can also find more examples in cbmc/regression/contracts-dfcc/loop_* benchmarks.

In your example, the clause __CPROVER_ensures is for function contracts. You may want to use loop contract clauses __CPROVER_loop_invariant instead.

from cbmc.

Yes, CBMC support loop contracts to prove loops inductively: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/contracts/doc/user/contracts-loop-invariants.md. You can also find more examples in cbmc/regression/contracts-dfcc/loop_* benchmarks.

In your example, the clause __CPROVER_ensures is for function contracts. You may want to use loop contract clauses __CPROVER_loop_invariant instead.

Thank you for the reply! In my harness I used __CPROVER_loop_invariant( 0 <= i && i < cbData ) and __CPROVER_decreases( cbData - i ) but CBMC still tries to unwind the loop more than once. Am I still missing something for the invariant?

from cbmc.

Yes, CBMC support loop contracts to prove loops inductively: https://github.com/diffblue/cbmc/blob/develop/src/goto-instrument/contracts/doc/user/contracts-loop-invariants.md. You can also find more examples in cbmc/regression/contracts-dfcc/loop_* benchmarks.
In your example, the clause __CPROVER_ensures is for function contracts. You may want to use loop contract clauses __CPROVER_loop_invariant instead.

Thank you for the reply! In my harness I used __CPROVER_loop_invariant( 0 <= i && i < cbData ) and __CPROVER_decreases( cbData - i ) but CBMC still tries to unwind the loop more than once. Am I still missing something for the invariant?

After running goto-cc to generate the corresponding a.goto on your c code, you can then run

goto-instrument --dfcc $(TARGET)_harness --apply-loop-contracts a.out b.out

to instrument loop contracts in a.out and generate b.out, where $(TARGET)_harness is the name of your harness and should be harness in your example. Then running

cbmc b.out

will prove the harness with loop contracts.

If you don't want to use dynamic frame condition checking (https://diffblue.github.io/cbmc/contracts-dev-spec-dfcc.html), instrumenting loop contracts with

goto-instrument  --apply-loop-contracts a.out b.out

instead.

from cbmc.

@qinheping I'm using cbmc-starter-kit to run the proof and I added the --apply-loop-contracts flag to the makefile. I have another proof for SymCryptMd2, and I annotated loop invariants for this loop in SymCryptMd2AppendBlocks in the hope that CBMC does not need to unwind 18*48 times:

        t = 0;
        for( j=0; j<18; j++ )
        __CPROVER_loop_invariant(0 <= j < 18)
        __CPROVER_decreases(18 - j)
        {
            for( k=0; k<48; k++ )
            __CPROVER_loop_invariant(0 <= k < 48)
            __CPROVER_decreases(48 - k)
            {
                t = pChain->X[k] ^ SymCryptMd2STable[t];
                pChain->X[k] = (BYTE) t;
            }
            t = (t + j)& 0xff;
        }

but when I run make goto-instrument reported the following error:

[9/16] SymCryptMd2: checking function contracts                                                                                                                                                                          FAILED: /home/jiggly/test-cbmc/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness0600.goto /tmp/litani/runs/1ff454d7-40fb-4fce-b0e7-ba48e7025770/status/63e5961c-a1ae-4ea1-bd00-e4ad34f4e6be.json 

/usr/libexec/litani/litani exec --command 'goto-instrument      --apply-loop-contracts /home/jiggly/test-cbmc/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness0500.goto /home/jiggly/test-cbmc/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness0600.goto' --pipeline-name SymCryptMd2 --ci-stage build --job-id 63e5961c-a1ae-4ea1-bd00-e4ad34f4e6be --stdout-file /home/jiggly/test-cbmc/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/logs/check_function_contracts-log.txt --description 'SymCryptMd2: checking function contracts' --status-file /tmp/litani/runs/1ff454d7-40fb-4fce-b0e7-ba48e7025770/status/63e5961c-a1ae-4ea1-bd00-e4ad34f4e6be.json --profile-memory-interval 10 --inputs /home/jiggly/test-cbmc/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness0500.goto --outputs /home/jiggly/test-cbmc/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness0600.goto

--- begin invariant violation report ---

Invariant check failed

File: ../src/goto-instrument/contracts/instrument_spec_assigns.h:286 function: update

Condition: source_location.is_not_nil()

Reason: Precondition

Backtrace:

goto-instrument(+0x902510) [0x5571b6055510]

goto-instrument(+0x9031e9) [0x5571b60561e9]

goto-instrument(+0x185244) [0x5571b58d8244]

goto-instrument(+0x2fedcd) [0x5571b5a51dcd]

goto-instrument(+0x2fc09b) [0x5571b5a4f09b]

goto-instrument(+0x2fd11e) [0x5571b5a5011e]

goto-instrument(+0x277f82) [0x5571b59caf82]

goto-instrument(+0x27d228) [0x5571b59d0228]

goto-instrument(+0x27d8b0) [0x5571b59d08b0]

goto-instrument(+0x18abcd) [0x5571b58ddbcd]

goto-instrument(+0x18ec17) [0x5571b58e1c17]

goto-instrument(+0x182a2f) [0x5571b58d5a2f]

goto-instrument(+0x172a69) [0x5571b58c5a69]

/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x7f6ee96e0d90]

/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x7f6ee96e0e40]

goto-instrument(+0x184295) [0x5571b58d7295]





--- end invariant violation report ---

Aborted

ninja: build stopped: cannot make progress due to previous errors.

from cbmc.

I tried to reproduced the issue with a smaller example and observed the same error.

typedef unsigned SIZE_T;
typedef uint8_t BYTE;
typedef BYTE *PBYTE;
typedef const BYTE *PCBYTE;
#define NULL ((void *)0)
#define SYMCRYPT_MD2_RESULT_SIZE (16)
#define SYMCRYPT_MD2_INPUT_BLOCK_SIZE (16)

const BYTE SymCryptMd2STable[256] = {
  41,  46,  67,  201, 162, 216, 124, 1,   61,  54,  84,  161, 236, 240, 6,
  19,  98,  167, 5,   243, 192, 199, 115, 140, 152, 147, 43,  217, 188, 76,
  130, 202, 30,  155, 87,  60,  253, 212, 224, 22,  103, 66,  111, 24,  138,
  23,  229, 18,  190, 78,  196, 214, 218, 158, 222, 73,  160, 251, 245, 142,
  187, 47,  238, 122, 169, 104, 121, 145, 21,  178, 7,   63,  148, 194, 16,
  137, 11,  34,  95,  33,  128, 127, 93,  154, 90,  144, 50,  39,  53,  62,
  204, 231, 191, 247, 151, 3,   255, 25,  48,  179, 72,  165, 181, 209, 215,
  94,  146, 42,  172, 86,  170, 198, 79,  184, 56,  210, 150, 164, 125, 182,
  118, 252, 107, 226, 156, 116, 4,   241, 69,  157, 112, 89,  100, 113, 135,
  32,  134, 91,  207, 101, 230, 45,  168, 2,   27,  96,  37,  173, 174, 176,
  185, 246, 28,  70,  97,  105, 52,  64,  126, 15,  85,  71,  163, 35,  221,
  81,  175, 58,  195, 92,  249, 206, 186, 197, 234, 38,  44,  83,  13,  110,
  133, 40,  132, 9,   211, 223, 205, 244, 65,  129, 77,  82,  106, 220, 55,
  200, 108, 193, 171, 250, 36,  225, 123, 8,   12,  189, 177, 74,  120, 136,
  149, 139, 227, 99,  232, 109, 233, 203, 213, 254, 59,  0,   29,  57,  242,
  239, 183, 14,  102, 88,  208, 228, 166, 119, 114, 248, 235, 117, 75,  10,
  49,  68,  80,  180, 143, 237, 31,  26,  219, 153, 141, 51,  159, 17,  131,
  20};
typedef struct
{
  BYTE C[16]; // State for internal checksum computation
  BYTE X[48]; // State for actual hash chaining
} STATE;

void SymCryptMd2AppendBlocks(
  STATE *pChain,
  PCBYTE pbData,
  SIZE_T cbData,
  SIZE_T *pcbRemaining)
{
  //
  // For variable names see RFC 1319.
  //
  unsigned int t;
  int j, k;

  while(cbData >= SYMCRYPT_MD2_INPUT_BLOCK_SIZE)
  {
    BYTE L;
    L = pChain->C[15];

    for(j = 0; j < 16; j++)
    {
      pChain->C[j] = L =
        pChain->C[j] ^ SymCryptMd2STable[L ^ pChain->X[16 + j]];
    }

    t = 0;
    for(j = 0; j < 18; j++)
      __CPROVER_loop_invariant(0 <= j < 18) __CPROVER_decreases(18 - j)
      {
        for(k = 0; k < 48; k++)
          __CPROVER_loop_invariant(0 <= k < 48) __CPROVER_decreases(48 - k)
          {
            t = pChain->X[k] ^ SymCryptMd2STable[t];
            pChain->X[k] = (BYTE)t;
          }
        t = (t + j) & 0xff;
      }

    pbData += SYMCRYPT_MD2_INPUT_BLOCK_SIZE;
    cbData -= SYMCRYPT_MD2_INPUT_BLOCK_SIZE;
  }

  *pcbRemaining = cbData;
}
void main()
{
  SIZE_T cbData; // unconstrained value
  SIZE_T *pcbRemaining;
  PBYTE pbData;
  BYTE abResult[SYMCRYPT_MD2_RESULT_SIZE];
  __CPROVER_assume(cbData <= 8);
  pbData = malloc(cbData);

  BYTE C[16]; // State for internal checksum computation
  BYTE X[48]; // State for actual hash chaining
  STATE state = {C, X};

  __CPROVER_assume(pbData != NULL);

  SymCryptMd2AppendBlocks(&state, pbData, cbData, pcbRemaining);

  free(pbData);
}

I believe the issue is caused by writing to field X of struct pChain in the loop.
While I am fixing the issue, could you try to use dfcc loop contracts instead? I didn't get the error with dfcc enabled. You can use dfcc by adding the dfcc flag before --apply-loop-contracts. It will be

goto-instrument --dfcc HARNESS_NAME  --apply-loop-contracts goto.out

Where HARNESS_NAME is the name of the harness function, and should be harness in SymCryptMd2.

You may also want to write loop contracts for the outer while-loop to avoid long verification time.

from cbmc.

Thank you @qinheping. So I added the --dfcc flag but the pipeline failed at the checking property step, and I saw the warning that the loops are missing assigns clauses. I followed the __CPROVER_assigns documentation and added the clauses as below but received parsing error.
Assign clause warning:

Failed property check(I also tried reducing the checks to only --bound-check but still failed):

I added assigns clause to the following three loops:
In the harness:

VOID
SYMCRYPT_CALL
SymCryptWipeAsm( _Out_writes_bytes_( cbData ) PVOID pbData, SIZE_T cbData )
{
    volatile BYTE * p = (volatile BYTE *) pbData;
    SIZE_T i;

    __CPROVER_assume( pbData != NULL );
    __CPROVER_assume( __CPROVER_w_ok( pbData, cbData ) );
    

    for( i=0; i<cbData; i++ )
    __CPROVER_loop_invariant( 0 <= i && i < cbData )
    __CPROVER_decreases( cbData - i )
    __CPROVER_assigns( __CPROVER_typed_target(p[i]) )
    {
        p[i] = 0;
    }

}

In md2.c SymCryptMd2AppendBlocks:

        t = 0;
        for( j=0; j<18; j++ )
        __CPROVER_assigns(__CPROVER_typed_target(t))
        __CPROVER_loop_invariant(0 <= j < 18)
        __CPROVER_decreases(18 - j)
        {
            for( k=0; k<48; k++ )
            __CPROVER_assigns(__CPROVER_typed_target(t))
            __CPROVER_assigns(__CPROVER_typed_target(pChain->X[k]))
            __CPROVER_loop_invariant(0 <= k < 48)
            __CPROVER_decreases(48 - k)
            {
                t = pChain->X[k] ^ SymCryptMd2STable[t];
                pChain->X[k] = (BYTE) t;
            }
            t = (t + j)& 0xff;
        }

Assigns clause parsing error:

I'm running CBMC 6.0.1 right now.

from cbmc.

Loop contracts have to be specified in order. __CPROVER_assigns must be specified before __CPROVER_loop_invariant. That is, it should be

    for( i=0; i<cbData; i++ )
    __CPROVER_assigns( __CPROVER_typed_target(p[i]) )
    __CPROVER_loop_invariant( 0 <= i && i < cbData )
    __CPROVER_decreases( cbData - i )
    {
        p[i] = 0;
    }

from cbmc.

I've switch the order but the error persists. You can see from the parsing error it's referring to the line pChaint->X[k] and the assign clause precedes the other statements.

from cbmc.

Failed property check(I also tried reducing the checks to only --bound-check but still failed):

Could you provide more detail about the failure by running the command after /usr/libexec/litani/litani exec --command?

Assigns clause parsing error:

Sorry I didn't notice that you write two assigns clauses for one loop. All assign targets must be specified in one assign clause, for example

for( k=0; k<48; k++ )
            __CPROVER_assigns(__CPROVER_typed_target(t), __CPROVER_typed_target(pChain->X[k]))
            __CPROVER_loop_invariant(0 <= k < 48)
            __CPROVER_decreases(48 - k)
            {
                t = pChain->X[k] ^ SymCryptMd2STable[t];
                pChain->X[k] = (BYTE) t;
            }
            t = (t + j)& 0xff;

from cbmc.

With the assign clauses now and --dfcc and --apply-loop-contract there is no direct failure but the report is giving me the following warning and errors:

Partial trace for first error:

Partial trace for second error:

SymCryptWipeAsm:

With the error CBMC stops at the SymCryptWipeAsm function and does not look further which causes poor coverage.
This is proof for SymCryptMd2 and the full harness is here
I've been getting stuck on this simple function for two weeks now and it seems like it shouldn't be too complicated to make it inductive... My ultimate goal is for CBMC to not give unwinding failure since cbData is of size_t and can be very large. Appreciate any guidance^_^

from cbmc.

You should look at the "init_st" function in my cbmc-examples repository, which does almost exactly the same time.
The specification with pre- and post-condition is here:
https://github.com/rod-chapman/cbmc-examples/blob/b8d5caf4fb39148084511200e1676615e91aefea/arrays/ar.h#L77
the body is here:
https://github.com/rod-chapman/cbmc-examples/blob/b8d5caf4fb39148084511200e1676615e91aefea/arrays/ar.c#L169

Using CBMC 6.0.0, if I run:

make TARGET=init_st

the output concludes:

** 0 of 1246 failed (1 iterations)
VERIFICATION SUCCESSFUL

from cbmc.

I assed a "zero_slice()" function, which is closer to your example.
Specification: https://github.com/rod-chapman/cbmc-examples/blob/823a7094e9dfa3426b1892aa364bdc5febbdf28b/arrays/ar.h#L82
Body: https://github.com/rod-chapman/cbmc-examples/blob/823a7094e9dfa3426b1892aa364bdc5febbdf28b/arrays/ar.c#L181

Just do
"make TARGET=zero_slice"
to see the proof.

from cbmc.

Thank you @rod-chapman! Using __CPROVER_object_upto() resolved the assignable error, but the first error(Check invariant after step for loop) still persists:

My updated harness:

VOID
SYMCRYPT_CALL
SymCryptWipeAsm( _Out_writes_bytes_( cbData ) PVOID pbData, SIZE_T cbData )
{
    volatile BYTE * p = (volatile BYTE *) pbData;
    SIZE_T i;

    for( i=0; i<cbData; i++ )
    __CPROVER_assigns( __CPROVER_typed_target(i), __CPROVER_object_upto(p, cbData) )
    __CPROVER_loop_invariant( i < cbData ) // also tried __CPROVER_loop_invariant( 0 <= i && i < cbData )
    __CPROVER_loop_invariant(__CPROVER_forall { size_t j; (0 <= j && j < i) ==> p[j] == 0 } )
    __CPROVER_decreases( cbData - i ) 
    {
        p[i] = 0;
    }

}

I'm not sure what the error itself means. Is it saying that we should only check invariant after the loop has started or we should not?

from cbmc.

@qinheping I was looking at the proofs for aws c common and aws encryption sdk and it looks like they didn't turn on the --apply-loop-contract, --dfcc or function contract flag, and there was not use of __CPROVER_loop_invariant() clauses. In addition, the unwind flag in Makefile.common are both set to 1. I would imagine unwind bound of 1 would be too small for a lot of the loops and without applying loop contracts how were they able to not get any unwind failure errors?

from cbmc.

Also I'm getting a lot of warning:


I'm not sure what caused these warnings and is there anyway to correct or supress these warnings? Thanks!

from cbmc.

@qinheping I was looking at the proofs for aws c common and aws encryption sdk and it looks like they didn't turn on the --apply-loop-contract, --dfcc or function contract flag, and there was not use of __CPROVER_loop_invariant() clauses.

You can find the unbounded proof of aws c common here. However, the proofs only use old loop contracts but not dfcc.

In addition, the unwind flag in Makefile.common are both set to 1. I would imagine unwind bound of 1 would be too small for a lot of the loops and without applying loop contracts how were they able to not get any unwind failure errors?

The actual unwinding bounds are specified for each proof separately in the variable UNWINDSET in makefile. https://github.com/search?q=repo%3Aaws%2Faws-encryption-sdk-c+unwindset&type=code.

from cbmc.

Also I'm getting a lot of warning: I'm not sure what caused these warnings and is there anyway to correct or supress these warnings? Thanks!

The third warning ignoring forall. The SAT backend eagerly grounds quantifiers when domains are small, but ignores them when domains are too large, which is seems to be the case here. Is there any quantifier __CPROVER_forall in your code? If yes, you should try using the SMT back-end, z3 for example, by adding the flag --smt2 to the CBMC command.

For the first two warnings, there are duplicate functions. @tautschnig , what is the right way to supress the duplicate symbol warning?

from cbmc.

1. You should always use --smt2 with quantifiers.
2. In my cbmc-examples repo, all the functions use contracts, loop invariants and unbounded verification. I hope to expand these to cover more cases as I go along.

I could point you at an entire crypto library that has sound, unbounded verification of type safety, but it ain't C.. :-)

from cbmc.

I could point you at an entire crypto library that has sound, unbounded verification of type safety, but it ain't C.. :-)

😮 @rod-chapman Could you still give me the reference? What language is it in and what's the verification tool?

from cbmc.

The execution failed after switching to --smt2 😿
Failed command: cbmc --flush --unwind 1 --unwinding-assertions --smt2 --bounds-check --trace --xml-ui /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness.goto

Upon checking the log the solver had an error in this step:

from cbmc.

The execution failed after switching to --smt2 😿 Failed command: cbmc --flush --unwind 1 --unwinding-assertions --smt2 --bounds-check --trace --xml-ui /home/jiggly/SymCrypt-CBMC/CBMC/proofs/SymCryptMd2/gotos/SymCryptMd2_harness.goto Upon checking the log the solver had an error in this step:

The image tells that there is some error when running SMT2 solver, but it doesn't show the actual error.I suppose it is the same issue as #8329. Could you find and share the accrual error message. Searching for SMT2 solver returned error message: might help.

from cbmc.

@qinheping I believe it's the same issue with #8329 since I'm also using the for_all statement in a similar way:

VOID
SYMCRYPT_CALL
SymCryptWipeAsm( _Out_writes_bytes_( cbData ) PVOID pbData, SIZE_T cbData )
{
    volatile BYTE * p = (volatile BYTE *) pbData;
    SIZE_T i;

    for( i=0; i<cbData; i++ )
    __CPROVER_assigns( __CPROVER_typed_target(i), __CPROVER_object_upto(p, cbData) )
    __CPROVER_loop_invariant( i < cbData ) // also tried __CPROVER_loop_invariant( 0 <= i && i < cbData )
    __CPROVER_loop_invariant(__CPROVER_forall { size_t j; (0 <= j && j < i) ==> p[j] == 0 } ) // forall x. e1 => e2
    __CPROVER_decreases( cbData - i ) 
    {
        p[i] = 0;
    }

}

What's the best approach right now? If SAT and SMT both are not able to evaluate the for_all statment correctly is there another way to make this loop inductive? I just tried switching back to SAT and re-run the proof for SymCryptMd2 and it gave the following errors:

The induction error persists

And I borrowed the stub for memcpy from aws and I'm not sure what triggered these errors and what need to be done in general to prevent these type of dereference failures:

Also the __CPROVER_contracts library also has some complaints(is this the result of using the inadequate solver?):

from cbmc.