OpenSSL Typestate analysis Secure Memory check bug

[Ayohbk]

• [x] I have searched open and closed issues for duplicates
• [x] I made sure that I am not using an old project version (DO: pull Phasar, update git submodules, rebuild the project and check if the bug is still there)

---

Bug description

Incorrrect result reported by the IDESolver for IDETypeStateProblem with TypeDescription set to OpenSSLSecureMemoryDescription.

For this secure memory program code memory2.c , no error state is detected when the IDETypeStateAnalysis is executed. However, if the same code is duplicated and set in both if and else blocks and the analysis is executed. The observed result shows error state detected. The expected result is no error state detected.

This issue was detected during the implementation of our academic project PhASIO . We have also discussed this issue with Martin and Phillip.

Steps to reproduce

• Replace the file in myphasartool.cpp with the myphasartool.cpp file in the attached zip folder.
• Trigger compilation and generate the myphasartool binary.
• Generate LLVM IR file ifmemory.ll for the program ifmemory.c also contained in the attached zip folder.
• Run the command myphasartool ifmemory.ll

Actual result: Error state detected. ( Our generated results dump file "SecureMemorySolverResultsDump.txt" is in the attached zip folder)

Expected result: No error state detected.

Context (Environment)

Operating System:

• [x] Linux
• [ ] Windows
• [ ] macOS

Build Type:

• [x] cmake
• [ ] custom build

Possible solution

We are happy to discuss possible solutions to this problem, especially if it origniates from a design flaw.

Example files

SecureMemoryIssue.zip

Files:

[fabianbs96]

Hi @Ayohbk, I could reproduce your bug. It appears that the analysis is indeed correct here. This is, because it cannot know that the function CRYPTO_malloc is a memory allocator and thus the returned pointers never alias (point to the same memory address). Therefore, the analysis must assume the worst-case (where buffer and buffer1 are aliases). When now calling CRYPTO_free in either branch, only one of buffer and buffer1 is initialized. Hence, the analysis detects two errors:

• If value > 3: Call to CRYPTO_free on the uninitialized buffer1 aliased by buffer
• If value >= 3: Call to CRYPTO_free on the uninitialized buffer aliased by buffer1

Unfortunately, we cannot fix this issue because currently we use the alias-analysis provided by LLVM. A possible fix would be adding __attribute__((malloc)) to the CRYPTO_malloc function declaration in the OpenSSL header. This would result in a minor difference in the function declaration in the IR: declare dso_local noalias i8* @CRYPTO_malloc(i64, i8*, i32). I have checked, that the analysis indeed reports no error on the modified IR. You can try it yourself by simply add the noalias attribute to CRYPTO_malloc in your IR file.