Dynamic array lengths

[bjohannesmeyer]

Is it possible to verify a function with a variable length array input? All of the examples use constant lengths for __SMACK_values. For example, in the following code there is a branch on an array value that may be public depending on len:

#include "ct-verif.h"

void foo(int *x) {
        int a;
        if(x[0] == 7) a = 9*7;
}

void foo_wrapper(int *x, int len) {
        public_in(__SMACK_value(x));
        public_in(__SMACK_value(len));
        public_in(__SMACK_values(x,len));
        foo(x);
}

However SMACK generates an error in this case:

make[1]: Entering directory `/root/verifying-constant-time/bin'
Generating BPL model
smack.py -t  --verifier=boogie --entry-points foo_wrapper --unroll 1 --loop-limit 1 -bpl /root/verifying-constant-time/examples/dynarr/foo.bpl  /root/verifying-constant-time/examples/dynarr/foo.c
SMACK program verifier version 1.5.1
0  llvm2bpl        0x0000000000acd922 llvm::sys::PrintStackTrace(_IO_FILE*) + 34
1  llvm2bpl        0x0000000000acd714
2  libpthread.so.0 0x00002b75888e2330
3  llvm2bpl        0x00000000004f0024 smack::Regions::visitCallInst(llvm::CallInst&) + 276
4  llvm2bpl        0x00000000004ef85c smack::Regions::runOnModule(llvm::Module&) + 492
5  llvm2bpl        0x0000000000a72065 llvm::legacy::PassManagerImpl::run(llvm::Module&) + 693
6  llvm2bpl        0x00000000004edfc3 main + 1539
7  libc.so.6       0x00002b7589b96f45 __libc_start_main + 245
8  llvm2bpl        0x00000000004ed802
Stack dump:
0.      Program arguments: llvm2bpl /root/verifying-constant-time/bin/a-jJlRoL.bc -bpl /root/verifying-constant-time/examples/dynarr/foo.bpl -source-loc-syms -enable-type-inference-opts -entry-points foo_wrapper -mem-mod-impls 
1.      Running pass 'SMACK Memory Regions Pass' on module '/root/verifying-constant-time/bin/a-jJlRoL.bc'.
0  llvm2bpl        0x0000000000acd922 llvm::sys::PrintStackTrace(_IO_FILE*) + 34
1  llvm2bpl        0x0000000000acd714
2  libpthread.so.0 0x00002b75888e2330
3  llvm2bpl        0x00000000004f0024 smack::Regions::visitCallInst(llvm::CallInst&) + 276
4  llvm2bpl        0x00000000004ef85c smack::Regions::runOnModule(llvm::Module&) + 492
5  llvm2bpl        0x0000000000a72065 llvm::legacy::PassManagerImpl::run(llvm::Module&) + 693
6  llvm2bpl        0x00000000004edfc3 main + 1539
7  libc.so.6       0x00002b7589b96f45 __libc_start_main + 245
8  llvm2bpl        0x00000000004ed802
Stack dump:
0.      Program arguments: llvm2bpl /root/verifying-constant-time/bin/a-jJlRoL.bc -bpl /root/verifying-constant-time/examples/dynarr/foo.bpl -source-loc-syms -enable-type-inference-opts -entry-points foo_wrapper -mem-mod-impls 
1.      Running pass 'SMACK Memory Regions Pass' on module '/root/verifying-constant-time/bin/a-jJlRoL.bc'.

Error invoking command:
llvm2bpl /root/verifying-constant-time/bin/a-jJlRoL.bc -bpl /root/verifying-constant-time/examples/dynarr/foo.bpl -source-loc-syms -enable-type-inference-opts -entry-points foo_wrapper -mem-mod-impls
llvm2bpl returned non-zero.
make[1]: *** [/root/verifying-constant-time/examples/dynarr/foo.bpl] Error 1
make[1]: Leaving directory `/root/verifying-constant-time/bin'
make: *** [verify] Error 2

If instead a constant length is used --- e.g. public_in(__SMACK_values(x,2)); --- then it verifies. I imagine this would be impossible to verify since if the length is unknown, then it is unknown which array values are public, and thus it is impossible to know whether the branch is on a public or secret value. I just want to make sure I'm not missing something.

FWIW, I'm using the older versions of the tools (SMACK, Bam, Z3, Boogie) that are currently linked to from the repository. See my response here for more info on tool versions.

[fdupress]

These are issues with the version of Smack you are using not being able to parse more complex annotations. I realise that you cannot upgrade because of the fact that Bam does not compute the product program correctly when using the right version of Smack, and this is somewhere way deep in my stack of stuff to look at over the summer.

In fact, it would help float things to the top if you (or Mike) can give me a recipe to quickly get a Smack + Bam toolchain set up and working to get the unsound behaviour from #2 : I could then check out how annotations changed internally and patch bam to catch them again and emit the right assertions.

[michael-emmi]

Hey @fdupress are you saying that some version of Ct-Verif supported dynamic-length annotations?

I was under the impression that we had not implemented that, though I might be forgetting something.

[fdupress]

Hi @michael-emmi.

It did not, but that was mainly due to the fact that we had no annotation language for it. If Smack now eats these annotations and preserves them all the way to BoogiePL, I can look into extending the product generation, but it first needs to be fixed to work with the version of Smack that does not fail hard. (The same applies for nested structs.)