Verifying the function call sequence

[StanPlatinum]

In the context of security and C programs, one could tamper with the call stack. Guided by Prof. Rakamaric (boogie-org/boogie#191), we @ya0guang @Gao-Chuan notice that model stack behaviors can be introduced in the Boogie files generated by SMACK.
However, it may be a non-trivial work and hope we could do some help if this can be a future feature in SMACK’s memory safety check.

[Gao-Chuan]

For example, if we have a program like this:

#include <stdio.h>
#include <stdlib.h>

void __attribute__((stdcall))  fun(int k, int c, int d, int e, int f, int g, int h, int i, int j, int n, int l)
{
    l = 0xfff;
}



void  fun1(void (*pfun)(int), int a, char c)
{
    pfun(a);
}

int main()
{
    fun1(fun, 1, 'a');
    return 0;
}

gcc -m32 -g test.c -o test

There will be a Segmentation fault in x86 system.
The same thing will also happen on x64 as long as we make the parameter list long enough.

In this case, when eip return from fun() to fun1(), esp will point to main's stack frame:
Before:

After:

[shaobo-he]

@keram88 Any thoughts?

[ya0guang]

Another example:

#include <stdlib.h>


int foo() {
    int i;
    int* pi;

    pi = &i;
    pi += 12;
    *pi = 0;

    return 0;

}

int main() {
    foo();
    return 0;   
}

I messed up the return address (on stack) in foo, so returning to main will not be performed correctly and segmentation fault will be raised.

[shaobo-he]

Another example:

#include <stdlib.h>


int foo() {
    int i;
    int* pi;

    pi = &i;
    pi += 12;
    *pi = 0;

    return 0;

}

int main() {
    foo();
    return 0;   
}

I messed up the return address (on stack) in foo, so returning to main will not be performed correctly and segmentation fault will be raised.

For this example, SMACK should be able to report an error with the flag --memory-safety.