Taint example allows 2 opens

[jacereda]

If I add a second open(&sock) the example will compile happily. I tried to add a where !isopen(*self) to open and it won't compile. Then I added a static_attest(!isopen(&sock); after the sock declaration and I still get a function is unprovable error.

What am I doing wrong? How can I model the restriction that an already opened socket can't be opened again?

[aep]

Hi,

type state can only be added, never removed. All type state is cleared on mutation. however, during open() the pointer itself is not mutated, so they are the same value entering and exiting (same pointer) an attest(is_open()) will conflict with the where(!is_open()) resulting in an unsolvable ssa equation.

you can do the thing you want by creating a theory of values instead of a theory of pointers. the value is mutated inside open() (by setting *a to 1) so it can be assigned a new type state

theory is_open(int a) -> bool;

fn open(int mut* a)
    where !is_open(*a)
    model is_open(*a)
{
    *a = 1;
    static_attest(is_open(*a));
}

fn read(int require<open> mut* a) -> int
    where is_open(*a)
    model is_open(*a)
{
    return *a;
}

fn close(int mut* a)
    model !is_open(*a)
{
    *a = 0;
    static_attest(!is_open(*a));
}

fn main() {
    int mut x = 0;
    static_attest(!is_open(x));
    open(&x);
    read(&x);
    read(&x);

    // wont compile
    //open(&x);

    close(&x);
    open(&x);

}

[jacereda]

Thanks for the prompt response.

I'm not sure I follow. The Socket pointer isn't mutated in open, but the contents are, in the same way that the integer pointer of your previous example isn't mutated but the contents are. Am I missing something?

Here is a modified version of the example that seems to do what I want without resorting to change the type. Notice the *self = Socket{fd: 2}; part. If I change that to the old self->fd = 2; it won't pass.

Also notice that I changed the theory to receive a Socket instead of a Socket * and it's still happy. Is that normal? Or rather, is it normal that something like isopen(*self) is valid for a theory expecting a Socket *?

using <stdio.h>::{printf};

theory isopen(Socket s) -> bool;

struct Socket {
    int mut fd;
}

fn open(Socket mut* self)
    where !isopen(*self)
    model isopen(*self)
{
    *self = Socket{fd: 2};
    static_attest(isopen(*self));
}

fn read(Socket mut* self) -> int
    where isopen(*self)
    model isopen(*self)
{
    return self->fd;
}

fn close(Socket mut* self)
    where isopen(*self)
    model !isopen(*self)
{
    *self = Socket{fd: 0};
    static_attest(!isopen(*self));
}

export fn main() -> int {
    Socket mut sock = {0};
    static_attest(!isopen(sock));

    open(&sock);
    read(&sock);
    close(&sock);

    printf("hello taint\n");
    return 0;
}

[jacereda]

BTW, which language are you using for code blocks? I tried with rust but looks like you used something else.

[aep]

Am I missing something?

zetz is not an abstract type checker but uses the concrete C memory model. A theory foo(int x) will set typestate on the value of x, not the value of x a theory(int x) instead will set state on the value "1"

breaking this down in steps:

theory is_open(int * a) -> bool;

fn open(int mut * a)
    where !is_open(a)
    model is_open(a)
{
   /// *a is unknown value
   /// a is pointer value 0x93828
   /// with typestate !is_open(0x93828)

    *a = 1;

   /// a is still pointer value 0x93828
   /// with typestate !is_open(0x93828)

    static_attest(is_open(a));

   /// a is still pointer value 0x93828
   /// with typestate !is_open(0x93828) && is_open(0x93828)

   /// function is unsolveable
}

theory is_open(int  a) -> bool;

fn open(int mut * a)
    where !is_open(*a)
    model is_open(*a)
{
   /// a is pointer value 0x93828
   /// *a is unknown value
   /// with typestate !is_open(placeholder)

    *a = 1;

   /// *a is 1
   /// with all state cleared, since it changed

    static_attest(is_open(*a));

   /// a is value 1
   /// with typestate is_open(0x93828)

   /// model matches
}

without resorting to change the type

isopen(Socket s) is also a theory of values. its just a larger value ;) structs are values in C

Or rather, is it normal that something like isopen(self) is valid for a theory expecting a Socket ?

you changed the theory to take a value

   theory isopen(Socket s) -> bool;

no pointer there.

btw you probably want a stack constructor function here

fn open(Socket mut new* self)
    model isopen(*self)
{
    *self = Socket{fd: 2};
    static_attest(isopen(*self));
}

fn main() {
   new sock = open();
}

which language are you using for code blocks?

i usually use the C++ highlighter

[jacereda]

Thanks, that clarifies it a lot.

But I still have a hard time trying to figure out why changing theory isopen(Socket fd) -> bool to theory isopen(Socket * fd) -> bool in this program seems to behave exactly the same:

using <stdio.h>::{printf};

theory isopen(Socket fd) -> bool;

struct Socket {
    int fd;
}

fn open(Socket mut new* self)
    where !isopen(*self)
    model isopen(*self)
{
    *self = Socket{fd: 2};
    static_attest(isopen(*self));
}

fn read(Socket mut * self) -> int
    where isopen(*self)
    model isopen(*self)
{
    return self->fd;
}

fn close(Socket mut* self)
    where isopen(*self)
    model !isopen(*self)
{
    *self = Socket{fd: 0};
    static_attest(!isopen(*self));
}

export fn main() -> int {
    Socket mut sock;
    static_attest(!isopen(sock));
    open(&sock);
    close(&sock);
    open(&sock);
    read(&sock);
    close(&sock);
    static_assert(!isopen(sock));
    printf("hello taint\n");
    return 0;
}

Shouldn't it fail at things like isopen(*self), where we are passing a Socket value instead of a Socket*?

[aep]

oh i see. yeah uninterpreted theories don't actually check their argument type because they're opaque anyway.

also

sizeof(Socket *) == sizeof(Socket)

so this is perfectly valid but gets confusing in larger code bases when you get seemingly unrelated error messages from being unable to access a Socket * as struct.

The symbolic execution engine is pretty messy code already, so i'd rather delay solving this for quite a while, sorry

opened #114 to track the issue