Join GitHub today
GitHub is home to over 40 million developers working together to host and review code, manage projects, and build software together.Sign up
lack of padding model for unpacked structs leads to soundness issues #417
After some short tests and discussion with @danieldietsch, I have the impression that Ultimate currently has no model in place to calculate the actual memory contents and memory footprint of structs that have elements which mandate padding within the struct memory area. (In-depth background).
Compilers will add unused memory bytes within or at the end of a subset of structs to improve the alignment to address boundaries, which will directly influence both the memory contents at a certain memory offset as well as the reported size of the struct.
Although not all struct configurations will trigger padding, those that do have some unexpected properties:
This can lead to unexpected behavior and real-world vulnerabilities.
One subset of the possible issues is explained here, but there are other potential bugs, e.g. simply overwriting more memory in a buffer than expected or copying data in the wrong position when using manually calculated offsets that fail to take the padding into account.
Code-wise, declaring the struct as
Ultimate will likely need a reworked memory model for structs as well as some parameters to adjust the default behavior for special architectures/compiler behavior.
Although getting this "perfectly" right could become a complex task, I think there could be significant improvements with moderate efforts. Related topics likely include bit fields and other special memory behavior.
Code to illustrate the issue (feel free to modify and include this as a test case):
Ultimate fb97592 on the preprocessed (
This is the case for
On the upside, at least the calculation is fast (< 8s), which makes debugging this less painful.