vyre-libs 0.6.3

vyre Category A library ecosystem - pure-IR compositions over vyre-ops hardware primitives
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
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151

schema_version = 1

[[predicate]]
id = "auth_check_dominates"
module = "auth_check_dominates"
function = "auth_check_dominates"
op_id = "vyre-libs::security::auth_check_dominates"
operation = "bitset_and"
inputs = ["auth_doms", "sensitive_op_set"]
output = "out"
soundness = "Exact"
witness_fixture = "security/auth_check_dominates/basic_overlap"
weir_mapping = "dominance(auth_check, sensitive_operation)"
witness_lhs = [12]
witness_rhs = [10]
witness_expected = [8]

[[predicate]]
id = "buffer_size_check"
module = "buffer_size_check"
function = "buffer_size_check"
op_id = "vyre-libs::security::buffer_size_check"
operation = "bitset_and"
inputs = ["size_compared", "user_input_set"]
output = "out"
soundness = "Exact"
witness_fixture = "security/buffer_size_check/basic_overlap"
weir_mapping = "range_comparison(size_compared, user_input)"
witness_lhs = [12]
witness_rhs = [10]
witness_expected = [8]

[[predicate]]
id = "format_string_check"
module = "format_string_check"
function = "format_string_check"
op_id = "vyre-libs::security::format_string_check"
operation = "bitset_and_not"
inputs = ["format_arg_pts", "non_literal_set"]
output = "out"
soundness = "Exact"
witness_fixture = "security/format_string_check/basic_subtraction"
weir_mapping = "points_to(format_argument) minus non_literal"
witness_lhs = [15]
witness_rhs = [12]
witness_expected = [3]

[[predicate]]
id = "lock_dominates"
module = "lock_dominates"
function = "lock_dominates"
op_id = "vyre-libs::security::lock_dominates"
operation = "bitset_and"
inputs = ["lock_doms", "shared_access_set"]
output = "out"
soundness = "Exact"
witness_fixture = "security/lock_dominates/basic_overlap"
weir_mapping = "dominance(lock_acquire, shared_access)"
witness_lhs = [12]
witness_rhs = [10]
witness_expected = [8]

[[predicate]]
id = "path_canonical"
module = "path_canonical"
function = "path_canonical"
op_id = "vyre-libs::security::path_canonical"
operation = "bitset_and"
inputs = ["canonicalizer_dominates", "fs_op_set"]
output = "out"
soundness = "Exact"
witness_fixture = "security/path_canonical/basic_overlap"
weir_mapping = "dominance(path_canonicalizer, filesystem_operation)"
witness_lhs = [12]
witness_rhs = [10]
witness_expected = [8]

[[predicate]]
id = "sanitizer_dominates"
module = "sanitizer_dominates"
function = "sanitizer_dominates"
op_id = "vyre-libs::security::sanitizer_dominates"
operation = "bitset_and"
inputs = ["sanitizer_doms", "sink_set"]
output = "out"
soundness = "Exact"
witness_fixture = "security/sanitizer_dominates/basic_overlap"
weir_mapping = "dominance(sanitizer, sink)"
witness_lhs = [12]
witness_rhs = [10]
witness_expected = [8]

[[predicate]]
id = "sql_param_bound"
module = "sql_param_bound"
function = "sql_param_bound"
op_id = "vyre-libs::security::sql_param_bound"
operation = "bitset_and"
inputs = ["param_binding_set", "sql_query_set"]
output = "out"
soundness = "Exact"
witness_fixture = "security/sql_param_bound/basic_overlap"
weir_mapping = "dominance(sql_parameter_binding, query_execution)"
witness_lhs = [12]
witness_rhs = [10]
witness_expected = [8]

[[predicate]]
id = "taint_kill"
module = "taint_kill"
function = "taint_kill"
op_id = "vyre-libs::security::taint_kill"
operation = "bitset_and_not"
inputs = ["frontier_in", "kill_set"]
output = "frontier_out"
soundness = "Exact"
witness_fixture = "security/taint_kill/basic_subtraction"
weir_mapping = "frontier minus sanitizer_or_guard_kill_set"
witness_lhs = [15]
witness_rhs = [12]
witness_expected = [3]

[[predicate]]
id = "unchecked_return"
module = "unchecked_return"
function = "unchecked_return"
op_id = "vyre-libs::security::unchecked_return"
operation = "bitset_and_not"
inputs = ["use_set", "check_dominates"]
output = "out"
soundness = "Exact"
witness_fixture = "security/unchecked_return/basic_subtraction"
weir_mapping = "return_value_use minus dominance(check, use)"
witness_lhs = [15]
witness_rhs = [12]
witness_expected = [3]

[[predicate]]
id = "xss_escape"
module = "xss_escape"
function = "xss_escape"
op_id = "vyre-libs::security::xss_escape"
operation = "bitset_and"
inputs = ["escape_dominates", "render_set"]
output = "out"
soundness = "Exact"
witness_fixture = "security/xss_escape/basic_overlap"
weir_mapping = "dominance(html_escape, render_sink)"
witness_lhs = [12]
witness_rhs = [10]
witness_expected = [8]