Vague error messages & Undefined behavior encountered

[Jerry-zhxf]

When using saw-script, I encountered two problems that could not be solved. I could not understand the meaning of these errors and speculated about the causes of the errors, but still did not solve them. So I wanted to ask for some help.

1. When I used chacha20.cry to verify my own algorithm, this error occurred. (Vague error messages)

Stack frame function_name 
​Allocations: 
​	StackAlloc 39 0x40[64] Mutable 16-byte-aligned internal
​	StackAlloc 38 0x4[64] Mutable 4-byte-aligned internal
                                ...

I don't understand what "internal" means which doesn't help debug at all. I've seen this error in some other problems, but their solution doesn't seem to work for me.Because the "memcpy_s" function is used in my chacha20, I guess it's a problem. However, the for loop assignment is still useless, and more errors are reported.
And I see some OpenSSL memory function verification in aws-lc-verification(aws-lc-verification\SAW\proof\common\memory.saw)), so I wonder if the saw implementation and proof of this memcpy function is missing. (But I haven't tried it yet. )

2. When I used SHA256.cry(cryptol-specs) to verify my own algorithm, this error occurred. (Undefined behavior encountered)

Subgoal failed: function_name safety assertion:
error: in memcpy_s
Undefined behavior encountered
Details:
​	Comparison of pointers from different allocations

The source address and destination address of the "memcpy_s" function should be different, but the error message is "Comparison of points from different allocations". I wonder if I need to describe the behavior of "memcpy_s" so that it can be trusted to avoid errors.

In aws-lc-verification, they are tested on the EVP interface, but I directly verify the underlying OpenSSL function interface. (For example, openssl\crypto\sha\sha256.c - SHA256_Init). Is this a problem? Since there are "memset" and "memcpy" proofs in the underlying functions that are not in aws-lc-verification\SAW\proof\common\memory.saw.

If you have free time, please help me, thank you very much!

[RyanGlScott]

I don't understand what "internal" means which doesn't help debug at all.

It's hard to know for sure without seeing the full example, but most likely, this is the result of the way SAW analyzes LLVM bitcode. When Clang compiles C code to LLVM bitcode, the LLVM bitcode will often stack-allocate memory that doesn't directly correspond to a line of code in the original C code. In these sorts of situations, SAW will simply report "internal" as the location of the stack-allocated memory, as it does not have a sensible place to point to in the original C program. It may be the case that further analysis could approximate the provenance of the stack-allocated memory, but in general, this is a tricky problem.

The source address and destination address of the "memcpy_s" function should be different, but the error message is "Comparison of points from different allocations".

Since you mentioned aws-lc-verification, it's possible that you may be running into #1308. There is a function called enable_lax_pointer_ordering that you can enable to allow SAW to perform pointer comparisons from different allocation units. While this is normally a suspect thing in most code, Clang often generates code which does this for performance reasons with -O2 or higher, so we added enable_lax_pointer_ordering to support this use case. (enable_lax_pointer_ordering could stand to be more publicly mentioned in the SAW manual, as it's currently undocumented.)

[robdockins]

If didn't compile with debug symbols, try that. The internal labels are used when the system doesn't know a source location for the associated allocation. Sometimes that's because the allocation was created by the system itself, but most often it's because there were no debug symbols to pull information from.

[Jerry-zhxf]

Thanks to both of you for your help, the problem is mostly solved.