Skip to content

Commit d4c01e9

Browse files
1022769410227694
committed
SDP Verification by TLA+
Signed-off-by: Luming Dong <[email protected]>
1 parent 75f2a7a commit d4c01e9

17 files changed

+2903
-0
lines changed

‎README.md

+1
Original file line numberDiff line numberDiff line change
@@ -109,6 +109,7 @@ Do you have your own case study that you like to share with the community? Send
109109
| 96 | Nano Blockchain Protocol | <a href="specifications/NanoBlockchain">Directory</a> | Andrew Helwer | | &#10004; | Naturals, Bags | | |
110110
| 97 | Coffee Can White/Black Bean Problem | <a href="specifications/CoffeeCan">Directory</a> | Andrew Helwer | | &#10004; | Naturals | | |
111111
| 98 | The Slush Protocol | <a href="specifications/SlushProtocol">Directory</a> | Andrew Helwer | | &#10004; | Naturals, FiniteSets, Sequences | &#10004; | |
112+
| 99 | SDP (Software Defined Perimeter) | <a href="https://github.com/10227694/SDP_Verification">Specifying and Verifying SDP Protocol based Zero Trust Architecture</a> | Luming Dong, Zhi Niu | | &#10004;| FiniteSets, Sequences, Naturals | |
112113

113114
## License
114115

‎specifications/README

+10
Original file line numberDiff line numberDiff line change
@@ -92,4 +92,14 @@ TwoPhase
9292
of the use of constant operator parameters to describe
9393
unspecified actions. There is also a TLA+ proof of
9494
correctness that has been checked by the TLAPS proof system.
95+
96+
SDP_Verification
97+
This project is about the TLA+ Spec of SDP architecture and algorithm
98+
written by Luming Dong and Zhi niu based on the open source project fwknop.
99+
The subdirectory SDP_Attack_Spec contains the specification based on the
100+
following materials:(* https://cloudsecurityalliance.org/artifacts/software-defined-perimeter-zero-trust-specification-v2/)(http://www.cipherdyne.org/fwknop/ *)
101+
The verification results show that current SDP protocol framework has a vulnerability
102+
in the scenario of remote access through NAT technology.
103+
The subdirectory SDP_Attack_New_Solution_Spec contains the specification for the improved
104+
SDP architecture design which fixed the flaw related to service concealment feature.
95105

‎specifications/SDP_Verification/LICENSE

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
MIT License
2+
3+
Copyright (c) 2022 Dong Luming
4+
5+
Permission is hereby granted, free of charge, to any person obtaining a copy
6+
of this software and associated documentation files (the "Software"), to deal
7+
in the Software without restriction, including without limitation the rights
8+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9+
copies of the Software, and to permit persons to whom the Software is
10+
furnished to do so, subject to the following conditions:
11+
12+
The above copyright notice and this permission notice shall be included in all
13+
copies or substantial portions of the Software.
14+
15+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
21+
SOFTWARE.

‎specifications/SDP_Verification/README.md

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
# SDP_Verification
2+
3+
This project is about the TLA+ Spec of SDP architecture and algorithm written by Luming Dong and Zhi niu based on the open source project fwknop.
4+
5+
The subdirectory SDP_Attack_Spec contains the specification based on the following materials:
6+
(* https://cloudsecurityalliance.org/artifacts/software-defined-perimeter-zero-trust-specification-v2/ *)
7+
(* http://www.cipherdyne.org/fwknop/ *)
8+
9+
The verification results show that current SDP protocol framework has a vulnerability in the scenario of remote access through NAT technology.
10+
11+
The subdirectory SDP_Attack_New_Solution_Spec contains the specification for the improved SDP architecture design
12+
which fixed the flaw related to service concealment feature.
13+
14+
The slide "Specifying and Verifying SDP Protocol Based Zero Trust Architecture Using TLA+.pptx" contains the key description of the reserach work.
15+
For details, please refer to paper :
16+
https://dl.acm.org/doi/10.1145/3558819.3558826
17+

‎specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/Comment.txt

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
The figure Model_Config_for_NAT.PNG illustrates the TLC model configuration for NAT scenario.
2+
3+
The figure Model_Config_without_NAT.PNG illustrates the TLC model configuration for scenario without NAT.
4+
5+
SPA_Attack_New.tla is the main sepc file.

‎specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/MC.cfg

+52
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
\* CONSTANT definitions
2+
3+
CONSTANT
4+
SDPSvrCfg <- const_1645172937699121000
5+
\* CONSTANT definitions
6+
7+
CONSTANT
8+
NAT_FLAG <- const_1645172937699122000
9+
\* CONSTANT definitions
10+
11+
CONSTANT
12+
USER_BASEPORT <- const_1645172937699123000
13+
\* CONSTANT definitions
14+
15+
CONSTANT
16+
MATCH_ANY <- const_1645172937699124000
17+
\* CONSTANT definitions
18+
19+
CONSTANT
20+
UNKNOWN_AUTH_ID <- const_1645172937699125000
21+
\* CONSTANT definitions
22+
23+
CONSTANT
24+
AttackerCfg <- const_1645172937699126000
25+
\* CONSTANT definitions
26+
27+
CONSTANT
28+
ClientCfg <- const_1645172937699127000
29+
\* CONSTANT definitions
30+
31+
CONSTANT
32+
ATTACKER_BASEPORT <- const_1645172937699128000
33+
\* CONSTANT definitions
34+
35+
CONSTANT
36+
SvrCfg <- const_1645172937699129000
37+
\* SPECIFICATION definition
38+
SPECIFICATION
39+
FairSpec
40+
\* INVARIANT definition
41+
INVARIANT
42+
SPASafeLaw
43+
DataAccessSafeLaw
44+
\* PROPERTY definition
45+
PROPERTY
46+
SPA_AvailableProperty
47+
SPA_AntiDosProperty
48+
UserAccessAvailProperty
49+
SvrHidenProperty
50+
FwRuleConsistentProperty
51+
FwCorrectProperty
52+
\* Generated on Fri Feb 18 16:28:57 CST 2022

‎specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/MC.tla

+51
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
---- MODULE MC ----
2+
EXTENDS SPA_Attack_New, TLC
3+
4+
\* CONSTANT definitions @modelParameterConstants:0SDPSvrCfg
5+
const_1645172937699121000 ==
6+
[IP |-> 12,Port |-> 8000]
7+
----
8+
9+
\* CONSTANT definitions @modelParameterConstants:1NAT_FLAG
10+
const_1645172937699122000 ==
11+
TRUE
12+
----
13+
14+
\* CONSTANT definitions @modelParameterConstants:2USER_BASEPORT
15+
const_1645172937699123000 ==
16+
1024
17+
----
18+
19+
\* CONSTANT definitions @modelParameterConstants:3MATCH_ANY
20+
const_1645172937699124000 ==
21+
65536
22+
----
23+
24+
\* CONSTANT definitions @modelParameterConstants:4UNKNOWN_AUTH_ID
25+
const_1645172937699125000 ==
26+
65535
27+
----
28+
29+
\* CONSTANT definitions @modelParameterConstants:5AttackerCfg
30+
const_1645172937699126000 ==
31+
[SrcIp |-> 11]
32+
----
33+
34+
\* CONSTANT definitions @modelParameterConstants:6ClientCfg
35+
const_1645172937699127000 ==
36+
[LoginID |->1,Key |-> 44,SrcIp |->11]
37+
----
38+
39+
\* CONSTANT definitions @modelParameterConstants:7ATTACKER_BASEPORT
40+
const_1645172937699128000 ==
41+
2024
42+
----
43+
44+
\* CONSTANT definitions @modelParameterConstants:8SvrCfg
45+
const_1645172937699129000 ==
46+
[IP |-> 22,Port |-> 80]
47+
----
48+
49+
=============================================================================
50+
\* Modification History
51+
\* Created Fri Feb 18 16:28:57 CST 2022 by 10227694

‎specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/Model_Config_for_NAT.PNG

34.3 KB
Loading

‎specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/Model_Config_without_NAT.PNG

43.3 KB
Loading

0 commit comments

Comments
 (0)