-- We abstract all users into two groups u and v; processes running on behalf of these groups are appropriately tagged at creation.
-- We model only the abstract categories uc, ut, vc, vt.
-- Labels are explicit in all these categories, i.e., they specify levels for all of these categories.

----------------------------
-- Principals and channels
----------------------------

-- generic process running on behalf of group u or v
-- LS.. defines a send label; LR.. defines a receive label; M.. encodes some data; Ready enables communication
new Useru(x), Ready(x), Mu(x), LSuc1(x), LSut1(x), LSvc1(x), LSvt1(x), LRuc2(x), LRut2(x), LRvc2(x), LRvt2(x) :- U.
new Userv(x), Ready(x), Mv(x), LSuc1(x), LSut1(x), LSvc1(x), LSvt1(x), LRuc2(x), LRut2(x), LRvc2(x), LRvt2(x) :- U.

-- net daemon
new NETd(x), LSuc1(x), LSut1(x), LSvc1(x), LSvt1(x), LRuc2(x), LRut2(x), LRvc2(x), LRvt2(x) :- U.

-- port uc/vc (on which data is sent over the net)
-- L.. defines a port label
new Portu(x), Luc0(x), Lut2(x), Lvc2(x), Lvt2(x) :- U. 
new Portv(x), Luc2(x), Lut2(x), Lvc0(x), Lvt2(x) :- U. 

-- net daemon assumes ownership of uc/vc.
next LSucSTAR(x), ~LSuc1(x) :- NETd(x), LSuc1(x), Portu(y).
next LSvcSTAR(x), ~LSvc1(x) :- NETd(x), LSvc1(x), Portv(y).

-- demux
new OKdemux(x), LSuc1(x), LSut1(x), LSvc1(x), LSvt1(x), LRuc2(x), LRut2(x), LRvc2(x), LRvt2(x) :- U.

-- Net daemon delegates ownership of uc/vc to demux.
next LSucSTAR(x), ~LSuc1(x) :- OKdemux(x), LSuc1(x), NETd(y), LSucSTAR(y).
next LSvcSTAR(x), ~LSvc1(x) :- OKdemux(x), LSvc1(x), NETd(y), LSvcSTAR(y).

-- Demux creates and assumes ownership of taint handle ut/vt.
next LSutSTAR(x), ~LSut1(x) :- OKdemux(x), LSut1(x), Useru(y).
next LSvtSTAR(x), ~LSvt1(x) :- OKdemux(x), LSvt1(x), Userv(y).

-- Demux delegates ownership of ut/vt to net daemon.
next LSutSTAR(x), ~LSut1(x), Ready(x) :- NETd(x), LSut1(x), OKdemux(y), LSutSTAR(y).
next LSvtSTAR(x), ~LSvt1(x), Ready(x) :- NETd(x), LSvt1(x), OKdemux(y), LSvtSTAR(y).

-- Net daemon raises its receive label to receive tainted data.
next LRut3(x), LRvt3(x), ~LRut2(x), ~LRvt2(x) :- NETd(x), LRut2(x), LRvt2(x), LSutSTAR(x), LSvtSTAR(x).

-- Net daemon raises labels of ports uc/vc to let them carry tainted data.
next Lut3(x), ~Lut2(x) :- Portu(x), Lut2(x), NETd(y), LucSTAR(y).
next Lvt3(x), ~Lvt2(x) :- Portv(x), Lvt2(x), NETd(y), LvcSTAR(y).

-- worker process for group u/v
new Wu(x), LSuc1(x), LSut1(x), LSvc1(x), LSvt1(x), LRuc2(x), LRut2(x), LRvc2(x), LRvt2(x) :- U.
new Wv(x), LSuc1(x), LSut1(x), LSvc1(x), LSvt1(x), LRuc2(x), LRut2(x), LRvc2(x), LRvt2(x) :- U.

-- Worker processes get tainted.
next LSucSTAR(x), LSut3(x), ~LSuc1(x), ~LSut1(x), Ready(x) :- Wu(x), LSuc1(x), LSut1(x), OKdemux(y), LSucSTAR(y), LSutSTAR(y).
next LSvcSTAR(x), LSvt3(x), ~LSvc1(x), ~LSvt1(x), Ready(x) :- Wv(x), LSvc1(x), LSvt1(x), OKdemux(y), LSvcSTAR(y), LSvtSTAR(y).

-- database proxy frontend (for receiving records)
new OKDBproxyDu(x), LSuc1(x), LSutSTAR(x), LSvc1(x), LSvtSTAR(x), LRuc2(x), LRut3(x), LRvc2(x), LRvt3(x) :- U.
new OKDBproxyDv(x), LSuc1(x), LSutSTAR(x), LSvc1(x), LSvtSTAR(x), LRuc2(x), LRut3(x), LRvc2(x), LRvt3(x) :- U.

-- ports on which records are received by database proxy
new PortDBu(x), Luc2(x), Lut3(x), Lvc2(x), Lvt2(x) :- U.
new PortDBv(x), Luc2(x), Lut2(x), Lvc2(x), Lvt3(x) :- U.

-- database proxy backend (for tainting and sending records)
new OKDBproxyWu(x), LSuc1(x), LSut3(x), LSvc1(x), LSvt3(x), LRuc2(x), LRut3(x), LRvc2(x), LRvt3(x) :- U.
new OKDBproxyWv(x), LSuc1(x), LSut3(x), LSvc1(x), LSvt3(x), LRuc2(x), LRut3(x), LRvc2(x), LRvt3(x) :- U.

-- generic unrestricted port
new PortUnrestricted(x), Luc3(x), Lut3(x), Lvc3(x), Lvt3(x) :- U.

-- universe of processes

SomeProc(x) :- Useru(x).
SomeProc(x) :- Userv(x).
SomeProc(x) :- NETd(x).
SomeProc(x) :- OKdemux(x).
SomeProc(x) :- Wu(x).
SomeProc(x) :- Wv(x).
SomeProc(x) :- OKDBproxyDu(x).
SomeProc(x) :- OKDBproxyDv(x).
SomeProc(x) :- OKDBproxyWu(x).
SomeProc(x) :- OKDBproxyWv(x).

-- universe of ports

SomePort(y) :- Portu(y).
SomePort(y) :- Portv(y).
SomePort(y) :- PortDBu(y).
SomePort(y) :- PortDBv(y).
SomePort(y) :- PortUnrestricted(y).

-------------------
-- Communication 
-------------------

-- Communication is possible only along the following links (from process x via port y to process z). 

Send(x,y,z) :- CanSend(x,y,z), Useru(x), PortUnrestricted(y), Wu(z), Ready(z).
Send(x,y,z) :- CanSend(x,y,z), Userv(x), PortUnrestricted(y), Wv(z), Ready(z).
Send(x,y,z) :- CanSend(x,y,z), NETd(x), Ready(x), PortUnrestricted(y), Ready(z).
Send(x,y,z) :- CanSend(x,y,z), NETd(x), Ready(x), PortUnrestricted(y), Ready(z).
Send(x,y,z) :- CanSend(x,y,z), Wu(x), Ready(x), Portu(y), Ready(z).
Send(x,y,z) :- CanSend(x,y,z), Wv(x), Ready(x), Portv(y), Ready(z).
Send(x,y,z) :- CanSend(x,y,z), Wu(x), Ready(x), PortUnrestricted(y), Wv(z), Ready(z).
Send(x,y,z) :- CanSend(x,y,z), Wv(x), Ready(x), PortUnrestricted(y), Wu(z), Ready(z).
Send(x,y,z) :- CanSend(x,y,z), Ready(x), PortDBu(y), OKDBproxyDu(z).
Send(x,y,z) :- CanSend(x,y,z), OKDBproxyDu(x), PortUnrestricted(y), OKDBproxyWu(z).
Send(x,y,z) :- CanSend(x,y,z), OKDBproxyWu(x), PortUnrestricted(y), Wu(z), Ready(z).
Send(x,y,z) :- CanSend(x,y,z), OKDBproxyWu(x), PortUnrestricted(y), Wv(z), Ready(z).
Send(x,y,z) :- CanSend(x,y,z), Ready(x), PortDBv(y), OKDBproxyDv(z).
Send(x,y,z) :- CanSend(x,y,z), OKDBproxyDv(x), PortUnrestricted(y), OKDBproxyWv(z).
Send(x,y,z) :- CanSend(x,y,z), OKDBproxyWv(x), PortUnrestricted(y), Wv(x), Ready(z).
Send(x,y,z) :- CanSend(x,y,z), OKDBproxyWv(x), PortUnrestricted(y), Wu(x), Ready(z).

-- Process x can send data on port y to process z if LS..(x) <= L..(y) /\ LR..(z).
-- We compute L..(y) /\ LR..(z) as RCV..(y,z).
-- We exploit the following information.
--   LS..c(x) \in {STAR,1}
--   LS..t(x) \in {STAR,1,3}
--   L..c(y) \in {STAR,0,2,3}
--   L..t(y) \in {2,3}
--   LR..c(z) \in {2}
--   LR..t(z) \in {2,3}

<SCRIPT>

my %levels = ("STAR" => -1, "0" => 0, "1" => 1, "2" => 2, "3" => 3);

for my $LSuc ("STAR", "1") {
for my $LSvc ("STAR", "1") {
for my $LSut ("STAR", "1", "3") {
for my $LSvt ("STAR", "1", "3") {
	print "CanSend(x,y,z) :- LSuc$LSuc(x), LSut$LSut(x), LSvc$LSvc(x), LSvt$LSvt(x), RCVuc$LSuc(y,z), RCVut$LSut(y,z), RCVvc$LSvc(y,z), RCVvt$LSvt(y,z).\n";
}
}
}	
}

print "\n";

for my $Lc ("STAR", "0", "2", "3") {
	for my $LRc ("2") {
		if ($levels{$Lc} <= $levels{$LRc}) { 
			print "RCVuc$Lc(y,z) :- Luc$Lc(y), LRuc$LRc(z).\n"; 
			print "RCVvc$Lc(y,z) :- Lvc$Lc(y), LRvc$LRc(z).\n"; 
		}
		else { 
			print "RCVuc$LRc(y,z) :- Luc$Lc(y), LRuc$LRc(z).\n"; 
			print "RCVvc$LRc(y,z) :- Lvc$Lc(y), LRvc$LRc(z).\n"; 
		}
	}
}

for my $Lt ("2", "3") {
	for my $LRt ("2", "3") {
		if ($levels{$Lt} <= $levels{$LRt}) { 
			print "RCVut$Lt(y,z) :- Lut$Lt(y), LRut$LRt(z).\n"; 
			print "RCVvt$Lt(y,z) :- Lvt$Lt(y), LRvt$LRt(z).\n"; 
		}
		else { 
			print "RCVut$LRt(y,z) :- Lut$Lt(y), LRut$LRt(z).\n"; 
			print "RCVvt$LRt(y,z) :- Lvt$Lt(y), LRvt$LRt(z).\n"; 
		}
	}
}

for my $i ("STAR", "0", "1") {
	my $j = $levels{$i} + 1;
	print "RCVuc$i(y,z) :- RCVuc$j(y,z).\n";
	print "RCVvc$i(y,z) :- RCVvc$j(y,z).\n";
}

for my $i ("STAR", "0", "1", "2") {
	my $j = $levels{$i} + 1;
	print "RCVut$i(y,z) :- RCVut$j(y,z).\n";
	print "RCVvt$i(y,z) :- RCVvt$j(y,z).\n";
}

</SCRIPT>

-- Process z receives data from process x and computes LS..(z) := LS..(z) \/ (LS..(x) /\ LS..*(z)).
-- We recognize categories in which the z's send label does not change after receiving from x as BasicSND..(z,x). 
-- Data M.. is transfered on communication.
-- Once again, we exploit information on label categories.

next Mu(z) :- Send(x,y,z), BasicSNDut(z,x), BasicSNDvt(z,x), Mu(x).
next LSvt3(z), ~LSvt1(z), Mu(z) :- Send(x,y,z), BasicSNDut(z,x), LSvt1(z), LSvt3(x), Mu(x).
next LSut3(z), ~LSut1(z), Mu(z) :- Send(x,y,z), LSut1(z), LSut3(x), BasicSNDvt(z,x), Mu(x).
next LSvt3(z), ~LSvt1(z), LSut3(z), ~LSut1(z), Mu(z) :- Send(x,y,z), LSut1(z), LSut3(x), LSvt1(z), LSvt3(x), Mu(x).

next Mv(z) :- Send(x,y,z), BasicSNDut(z,x), BasicSNDvt(z,x), Mv(x).
next LSvt3(z), ~LSvt1(z), Mv(z) :- Send(x,y,z), BasicSNDut(z,x), LSvt1(z), LSvt3(x), Mv(x).
next LSut3(z), ~LSut1(z), Mv(z) :- Send(x,y,z), LSut1(z), LSut3(x), BasicSNDvt(z,x), Mv(x).
next LSvt3(z), ~LSvt1(z), LSut3(z), ~LSut1(z), Mv(z) :- Send(x,y,z), LSut1(z), LSut3(x), LSvt1(z), LSvt3(x), Mv(x).

BasicSNDut(z,x) :- LSut3(z), LSut1(x).
BasicSNDut(z,x) :- LSut1(z), LSut1(x).
BasicSNDut(z,x) :- LSut3(z), LSut3(x).
BasicSNDut(z,x) :- LSutSTAR(z), SomeProc(x).
BasicSNDut(z,x) :- SomeProc(z), LSutSTAR(x).

BasicSNDvt(z,x) :- LSvt3(z), LSvt1(x).
BasicSNDvt(z,x) :- LSvt1(z), LSvt1(x).
BasicSNDvt(z,x) :- LSvt3(z), LSvt3(x).
BasicSNDvt(z,x) :- LSvtSTAR(z), SomeProc(x).
BasicSNDvt(z,x) :- SomeProc(z), LSvtSTAR(x).

--------------
-- Queries
--------------

SecrecyViolation :- Userv(x), Mu(x).
SecrecyViolation :- Wv(x), Mu(x).

? SecrecyViolation.