search

kenmcmil / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
77 stars 24 forks source link

Request for assistance in debugging: Verifying specifications for system with network-messaging #59

Closed prpr2770 closed 2 years ago

prpr2770 commented 2 years ago

The script that I'm trying to verify, is a connection-management protocol used by multiple-clients with one common server. The protocols consists of a two-way handshake. Connction-Request Message is sent by a client that is not connected to the Server. The Server may non-deterministically choose to either Accept the request or Reject it, by sending as a response the Connection-Accept message or a Connection-Reject message. The ivy-script for the same can be obtained here.

I'm having issues in debugging the type of failures indicated, as the structure of the network library, seems to be quite different from that of previous versions of IVy( < v1.8).

I have obtained the following error when checking the code using : ivy_check trace=true filename.ivy

    Any assertions in initializers must be checked ... PASS

    The following set of external actions must preserve the invariant:
        (internal) ext:client.hit
            connection_mgmt.ivy: line 87: client.invar300 ... PASS
        (internal) ext:client.server.sock.recv
            connection_mgmt.ivy: line 87: client.invar300 ... FAIL
searching for a small model... done
[
    index.succ(1,2) = true
    index.succ(0,1) = true
    index.succ(1,1) = false
    index.succ(1,0) = false
    index.succ(0,0) = false
    index.succ(0,2) = false
    index.succ(2,1) = false
    index.succ(2,0) = false
    index.succ(2,2) = false
    0:index = 0
    client_id.max = 0
    client.connected_clients(0) = true
    @X = 0
    client.sock.id(0) = 0
    client_id.succ(0,0) = false
    client.connectionRequested(0) = true
    client.pkt.kind(0) = conn_req
    client.pkt.kind(1) = conn_rej
    client.pkt.src_client(0) = 0
    client.pkt.src_client(1) = 0
    0:client_id = 0
    0:client_id < 0 = false
    1:index < 2 = true
    0:index < 1 = true
    0:index < 2 = true
    1:index < 1 = false
    1:index < 0 = false
    0:index < 0 = false
    2:index < 1 = false
    2:index < 0 = false
    2:index < 2 = false
    client.server.sock.id = 0
    client.net.tail(0,0) = 0
    client.connectionRejected(0) = false
    client.net.head(0,0) = 1
    client.connectionAccepted(0) = true
    client.net.sent(0,0,0,0) = true
    client.net.sent(0,0,2,0) = true
    client.net.sent(0,0,1,0) = false
    client.net.sent(0,0,1,1) = false
    client.net.sent(0,0,0,1) = false
    client.net.sent(0,0,2,1) = false
]
call client.server.sock.recv

{
    [
        fml:src = 0
        fml:msg = 0
    ]
/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 117: 
    assume client.net.tail(X,Y) <= client.net.head(X,Y)

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 118: 
    assume client.net.sent(X,Y,T,M1) & client.net.sent(X,Y,T,M2) -> M1 = M2

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 117: 
    assume client.net.tail(X,Y) <= client.net.head(X,Y)

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 118: 
    assume client.net.sent(X,Y,T,M1) & client.net.sent(X,Y,T,M2) -> M1 = M2

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 112: 
    assume client.net.tail(fml:src,client.server.sock.id) < client.net.head(fml:src,client.server.sock.id)

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 113: 
    assume client.net.sent(fml:src,client.server.sock.id,client.net.tail(fml:src,client.server.sock.id),fml:msg)

    [
        fml:y = 1
    ]
/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 114: 
    call client.net.tail(fml:src,client.server.sock.id) := index.next(client.net.tail(fml:src,client.server.sock.id))
    {
        [
            fml:x = 0
        ]
/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/order.ivy: line 38: 
        assume fml:x < fml:y & (fml:x < Y -> fml:y <= Y)

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/order.ivy: line 39: 
        assume index.succ(fml:x,fml:y)

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 117: 
        assume client.net.tail(X,Y) <= client.net.head(X,Y)

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 118: 
        assume client.net.sent(X,Y,T,M1) & client.net.sent(X,Y,T,M2) -> M1 = M2

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 117: 
        assume client.net.tail(X,Y) <= client.net.head(X,Y)

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 118: 
        assume client.net.sent(X,Y,T,M1) & client.net.sent(X,Y,T,M2) -> M1 = M2

    }

    [
        client.net.tail(0,0) = 1
    ]
connection_mgmt.ivy: line 122: 
    call client.server.recvin(fml:msg)
    {
        [
            fml:v = 0
        ]
        return

    }

connection_mgmt.ivy: line 138: 
    call client.connection_reject(client.pkt.src_client(fml:msg))
    {
        [
            fml:agent = 0
        ]
connection_mgmt.ivy: line 58: 
        assert ~client.connected_clients(fml:agent)

connection_mgmt.ivy: line 59: 
        assert client.connectionRequested(fml:agent) & ~client.connectionAccepted(fml:agent) & ~client.connectionRejected(fml:agent)

connection_mgmt.ivy: line 60: 
        client.connectionRejected(fml:agent) := true

        [
            client.connectionRejected(0) = true
        ]
    }

    [
        loc:msg = 0
    ]
connection_mgmt.ivy: line 140: 
    client.pkt.kind(loc:msg) := conn_rej

    [
        loc:msg = 1
    ]
connection_mgmt.ivy: line 141: 
    call client.server.sock.send(client.sock.id(client.pkt.src_client(fml:msg)), loc:msg)
    {
        [
            fml:dst = 0
            fml:msg_a = 1
        ]
/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 108: 
        client.net.sent(client.server.sock.id,fml:dst,client.net.head(client.server.sock.id,fml:dst),fml:msg) := true

        [
            client.net.sent(0,0,1,1) = true
            fml:y = 2
        ]
/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 109: 
        call client.net.head(client.server.sock.id,fml:dst) := index.next(client.net.head(client.server.sock.id,fml:dst))
        {
            [
                fml:x = 1
            ]
/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/order.ivy: line 38: 
            assume fml:x < fml:y & (fml:x < Y -> fml:y <= Y)

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/order.ivy: line 39: 
            assume index.succ(fml:x,fml:y)

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 117: 
            assume client.net.tail(X,Y) <= client.net.head(X,Y)

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 118: 
            assume client.net.sent(X,Y,T,M1) & client.net.sent(X,Y,T,M2) -> M1 = M2

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 117: 
            assume client.net.tail(X,Y) <= client.net.head(X,Y)

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 118: 
            assume client.net.sent(X,Y,T,M1) & client.net.sent(X,Y,T,M2) -> M1 = M2

        }

        [
            client.net.head(0,0) = 2
            fml:y = 1
        ]
/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 117: 
        assume client.net.tail(X,Y) <= client.net.head(X,Y)

/usr/local/lib/python2.7/dist-packages/ivy/include/1.8/network.ivy: line 118: 
        assume client.net.sent(X,Y,T,M1) & client.net.sent(X,Y,T,M2) -> M1 = M2

    }

    [
        loc:msg = 0
    ]
}
prpr2770 commented 2 years ago

As an alternative, when attempting to specify a ping-pong protocol, I've attempted two different representations, where I intend to use a transport-layer to send and receive messages.

When using a custom transport module that's been defined with a relation sent to keep track of the messages-that've been sent over the network, I can verify the system.

  1. The transport module definition
  2. The client-server ping-pong code that ivy_checks OK with v1.8.

However, when I modify the same, to ensure that I can use the network library, there are two failed checks. The script I'm using for the implementation of ping-pong using the network library is located here

prpr2770 commented 2 years ago

I got it to ivy_check OK and also, to compile and generate the test-scripts, by ensuring that I updated the gate-conditions within the sock.recv with the ghost-variables defined in the specification. The final verified script can be found here.