-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmg_auth.c.hquals
101 lines (81 loc) · 3.99 KB
/
mg_auth.c.hquals
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
//Index into context option array
qualif Option(v:int): v < 24
qualif ConfigArray(v:ptr): v + 96 <= BLOCK_END([v])
//Options Parsing
qualif VectorPtr(v:ptr, a:int): v != 0 => v + a <= BLOCK_END([v])
//Strings
constant STRING:func(1, [@(0);int])
qualif StringEq(v:ptr,s:ptr): STRING([v]) = STRING([s])
qualif StringEqWitness(v:int, p:ptr)://, q:ptr):
&&[v = 0;
? MUTABLE([BLOCK_BEGIN([p])]) => (0 = 1);
? MUTABLE([BLOCK_BEGIN([@f_])]) => (0 = 1)] =>
(STRING([p]) = STRING([@f_]))
//Qualifier for connections
constant CONN: func(1, [@(0);int])
qualif RequestMethodConn(v:ptr): (v != 0) => CONN([DEREF([v])]) = CONN([v])
qualif ConnEq(v:ptr,p:ptr): (v != 0) => CONN([v]) = CONN([p])
//Qualifiers for files
constant FILE: func(1, [@(0);int])
qualif FileEq(v:ptr,f:ptr): (v != 0) => FILE([v]) = FILE([f])
qualif PWFileEq(v:ptr,f:ptr): (v != 0) => && [FILE([DEREF([v + 0])]) = FILE([f]);
FILE([DEREF([v + 4])]) = FILE([f]);
FILE([DEREF([v + 8])]) = FILE([f])]
qualif FileOpen(v:ptr,p:ptr):
(?MUTABLE([BLOCK_BEGIN([p])]) => (0 = 1)) => (FILE([v]) = (p : int))
////Password Checking
constant PASSWORD_OK: func(1, [int;@(0);bool])
qualif PasswordOK(v:int,h:ptr): (v != 0) => ? PASSWORD_OK([CONN([@conn]);h])
qualif PasswordOK(v:int): (v != 0) => ? PASSWORD_OK([CONN([@conn]);@h])
//Connection Authorization
constant AUTHORIZED: func(1, [int;bool])
constant AUTHORIZED_BY: func(1, [int;int;bool])
qualif AuthorizedWitness(v:int,c:ptr): ? AUTHORIZED([CONN([c])])
qualif AuthorizedWitness(v:int,c:ptr): ? AUTHORIZED_BY([CONN([c]);FILE([@f])])
qualif AuthorizedCond(v:int): v != 0 => ? AUTHORIZED([CONN([@c])])
qualif AuthorizedByCond(v:int): v != 0 => ? AUTHORIZED_BY([CONN([@c]);FILE([@f])])
//PASSWD Files
constant PW_ENT: func(1, [@(0); @(1)])
constant AUTH_FILE: func(1, [int;int;bool])
qualif AuthFile(v:ptr): ?AUTH_FILE([CONN([@c]);FILE([v])])
qualif AuthorizedPut(v:int):
v != 0 => ? AUTHORIZED_BY([CONN([@c]);(DEREF([(DEREF([@c+20]):ptr)+8]):int)])
qualif PwEntry(v:ptr): v != 0 => &&[PW_ENT([DEREF([v])]) = v;
PW_ENT([DEREF([v+4])]) = v;
PW_ENT([DEREF([v+8])]) = v]
qualif PwEnt_Eq(v:ptr, w:ptr): PW_ENT([v]) = PW_ENT([w])
//Handy when parsing authorization header
qualif ParsedAH(v:int, a:ptr): (v != 0) =>
&&[DEREF([a+0]) > 0;
DEREF([a+4]) > 0;
DEREF([a+8]) > 0;
DEREF([a+12]) > 0;
DEREF([a+16]) > 0;
DEREF([a+20]) > 0;
DEREF([a+24]) > 0;
CONN([a]) = CONN([@conn]);
CONN([DEREF([a+0])]) = CONN([@conn]);
CONN([DEREF([a+4])]) = CONN([@conn]);
CONN([DEREF([a+8])]) = CONN([@conn]);
CONN([DEREF([a+12])]) = CONN([@conn]);
CONN([DEREF([a+16])]) = CONN([@conn]);
CONN([DEREF([a+20])]) = CONN([@conn]);
CONN([DEREF([a+24])]) = CONN([@conn])]
qualif Bool(v:int): ||[v = 0; v = 1]
qualif PutPasswdIdx(v:int): v = 8
qualif Err304(v:int): v = 304 => (?AUTHORIZED([CONN([@c])]))
constant NO_AUTHFILE: func(1, [int;bool])
constant NO_PROTECTFILE: func(1, [int;bool])
qualif NoAuthfile(v:ptr): v = 0 => ? NO_AUTHFILE([CONN([@c])])
qualif NoProtectfile(v:ptr): v = 0 => ? NO_PROTECTFILE([CONN([@c])])
qualif FpNullGPassNull(v:ptr): v = 0 => (DEREF([(DEREF([@c+20]):ptr)+44]) = 0)
qualif AuthFileDef(v:ptr): || [FILE([v]) = (DEREF([(DEREF([@c+20]):ptr)+44]) : int);
FILE([v]) = (DEREF([(DEREF([@c+20]):ptr)+8]) : int)]
qualif GlobalAuthFile(v:ptr): v = (DEREF([(DEREF([@c+20]):ptr)+44]) : int)
qualif PutAuthFile(v:ptr): v = (DEREF([(DEREF([@c+20]):ptr)+8]) : int)
qualif AuthFilePath(v:ptr): v != 0 => ? AUTH_FILE([CONN([@c]);(v:int)])
qualif AuthFileOpen(v:ptr): v != 0 => ? AUTH_FILE([CONN([@c]);FILE([v])])
qualif AuthFileWitness(v:int): ?AUTH_FILE([CONN([@c]);FILE([@r])])
qualif AuthFileWitness(v:int): ?AUTH_FILE([CONN([@c]);FILE([@f])])
constant URI: func(1, [@(0); int])
qualif ConnUri(v:ptr,c:ptr): URI([v]) = URI([c])