assura-stdlib 0.4.0

Assura standard library contracts and prelude types
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

// Standard library: network contracts
//
// Taint policy: recv produces @taint:untrusted output (network data is
// external). send requires @taint:validated input to prevent untrusted
// data from reaching network sinks without validation.
module std.net

contract connect {
    input(host: String, port: Nat)
    output(result: Int)
    requires { port > 0 }
    requires { host.length() > 0 }
    effects { net }
}

contract listen {
    input(port: Nat)
    output(result: Int)
    requires { port > 0 }
    effects { net }
}

contract send {
    input(handle: Int, data: Bytes @taint:validated)
    output(result: Nat)
    requires { data.length() > 0 }
    effects { net }
}

contract recv {
    input(handle: Int, max_bytes: Nat)
    output(result: Bytes)
    requires { max_bytes > 0 }
    effects { net }
    boundary { untrusted }
}

contract close_connection {
    input(handle: Int)
    output(result: Bool)
    effects { net }
}