[Question] Running CBMC on a C file with dynamic linking and/or shared libraries

[a-shokri]

Dear CBMC developers,

I have started using CBMC (6.4.1) to analyze the possibility of reaching and triggering a specific assertion in a C program. When working with a C program that includes only standard libraries or in case of non-standard library, the source code of the library is available, I can easily add the necessary paths to the command line, and CBMC works as expected. However, when the program depends on non-standard libraries via dynamic linking or shared libraries, CBMC logs multiple "no body" errors/warnings, indicating that it cannot find the implementation of certain functions.

This is problematic because if CBMC cannot resolve these functions, it cannot fully explore execution paths from the entry point to potential vulnerabilities or assertions, making the results unreliable.

My question is: apart from standard libraries, does CBMC always require access to the source files of all dependencies for the entry-point function's program? In other words, is there a way to introduce shared or pre-compiled libraries to CBMC without providing the source code of the dependencies?

Thank you in advance.

[tautschnig]

This is problematic because if CBMC cannot resolve these functions, it cannot fully explore execution paths from the entry point to potential vulnerabilities or assertions, making the results unreliable.

My question is: apart from standard libraries, does CBMC always require access to the source files of all dependencies for the entry-point function's program? In other words, is there a way to introduce shared or pre-compiled libraries to CBMC without providing the source code of the dependencies?

CBMC performs static analysis of C code. As such, it can neither rely on executing compiled code nor would it be able to decompile libraries back in to source code. For the C library CBMC comes with models of many functions to make up for this. For other libraries, as you said, you'd have to provide their source code. If such source code is not available to you, or possibly becomes to complex to analyse, you can provide your own stub implementations of those functions. When you do not provide such a stub (i.e., those cases where you saw the "no body" warnings), CBMC will assume the function to have no side effects and to return a non-deterministic value. Whether that is a good-enough assumption for your analysis only you can tell.