Execution of script taking more time.

[shashipattanshetty]

I implemented DRBG Generate function in C and Cryptol and used SAW script. After executing , it gives output :

[08:02:28.976] Verifying generate ...
[08:02:29.045] Simulating generate ...
[08:05:55.496] Checking proof obligations generate ...
[22:40:29.832]
*** Data.SBV: fd:5: hGetLine: end of file:

---

*** Sent : (check-sat)

---

*** Executable: /usr/bin/z3
*** Options : -nw -in -smt2

What is the issue here? Could you please help?

[weaversa]

What version of z3 do you have installed? What is the result of running this command in a terminal z3 —version ?

[shashipattanshetty]

Z3 version 4.8.7 - 64 bit

[robdockins]

It's a bit hard to provide more guidance without some more context. Can you provide the code you're working with?

As a general comment, it's sadly very common for an attempted program verification to generate proof obligation that is infeasible to solve. Breaking up the problem in a way that the solvers can actually complete their tasks in a reasonable amount of time is a bit of a black art. One easy thing to try is to attempt using different solvers; sometimes you get lucky and a different solver has an easier time solving your proof obligations.

[shashipattanshetty]

I tried the script with different solvers, it did not work. Here I have attached files containing DRBG_update function in C and Cryptol , and SAW Script.

Output was :

[warning] at ./AES128TBox.cry:266:83--266:84
This binding for i shadows the existing binding at
./AES128TBox.cry:264:9--264:10
[warning] at ./AES128TBox.cry:110:44--110:55:
Defaulting type argument 'ix' of '(Cryptol::@)' to 4
[warning] at ./AES128TBox.cry:115:30--115:41:
Defaulting type argument 'ix' of '(Cryptol::@)' to 4
[warning] at ./AES128TBox.cry:142:38--142:57:
Defaulting type argument 'ix' of '(Cryptol::@)' to 3
[warning] at ./AES128TBox.cry:166:38--166:57:
Defaulting type argument 'ix' of '(Cryptol::@)' to 3
[warning] at ./AES128TBox.cry:87:20--87:45:
Defaulting type argument 'rep' of 'Cryptol::number' to [4]
[warning] at ./AES128TBox.cry:71:50--71:55:
Defaulting type argument 'ix' of '(Cryptol::@)' to 9
[05:08:57.615] Printing
[05:08:57.615] Module: drbg_update.bc
Types:

Globals:
@sbox = internal default constant [256 x i8]
@rc = internal default constant [29 x i8]
@INV_SBOX = internal default constant [256 x i8]

External references:
declare void @llvm.dbg.declare(metadata, metadata, metadata)
declare i8* @calloc(i64, i64)

Definitions:
void @aes_key_schedule_256(i8* %0, i8* %1)
void @aes_encrypt_128(i8* %0, i8* %1, i8* %2)
internal void @shift_rows(i8* %0)
internal i8 @mul2(i8 %0)
void @aes_decrypt_256(i8* %0, i8* %1, i8* %2)
internal void @inv_shift_rows(i8* %0)
void @new_aes_encrypt_256(i8* %0, i8* %1, i8* %2)
i32 @wrapper_aes_encrypt_256(i8* %0, i8* %1, i8* %2)
i32 @drbg_update(i8* %0, i8* %1, i8* %2, i8* %3)
i32 @instantiate(i8* %0, i8* %1, i8* %2)

[05:08:57.615] drbg_update_spec
[05:08:57.615] <>
[05:08:57.615]

[05:08:57.644] Verifying drbg_update ...
[05:08:57.712] Simulating drbg_update ...
[05:09:10.176] Checking proof obligations drbg_update ...
Killed

Attachments :
1.aes.c - contains implementation of drbg_update function
2.aes.h - header file
3.AES128TBox.cry - contains implementation of drbg_update function in Cryptol
4.drbg_update.saw - SAW Script.
5. drbg_update_error.png - output of SAW script
drbg_update.zip

[Jerry-zhxf]

I also encountered the problem that the running time is too long. The verification of the aes algorithm has been running for more than a day. I still don't get the results now.

[09:38:36.218] Loading file "/home/saw-script/examples/openssl_aes/aes.saw"

[09:38:36.603] Verifying aes_encrypt ...
[09:38:36.603] Simulating aes_encrypt ...
[09:38:38.473] Checking proof obligations aes_encrypt ...

Is there something wrong with this?

[sauclovian-g]

Is this still relevant? It's been multiple years.

A quick look at the original example suggests that it's trying to do too much at once and should get broken down into multiple specifications for multiple functions.