--     
--  hardware     
--     

type network_comm is interface
-- type of plug for connections between networks and nodes     
    action out to_net  (data : Data; destination : Address);
    action in  to_node (data : Data; destination : Address);
end;

type user_comm is interface
-- type of plug for connections between users and nodes     
    action out to_user  (data : Data);
    action in  to_workstation (data : Data; destination : Address);
end;

type network_node is interface
-- the minimal interface of a node on a LAN
    provides        
        network_address : Address;
    service
	net_conn : network_comm;
end; 

type COTSWorkstation is 
interface
-- A C(ommercial O(ff) T(he) S(helf) Workstation
--	 is a node with a user interface
-- include  network_node;
    provides        
        network_address : Address;
    service
	net_conn  : network_comm;
-- end include network_node
    service
	user_conn : user_comm;
end;

module newCOTSWorkstation(address_  : Address) return COTSWorkstation is
        network_address : Address is address_;
-- This is a very simple skeleton of a workstation. 
-- It accepts data from the user to be transmitted onto the network,
-- and data from the network addressed to it, which it passes on to the user.
    action start_WS(Net : NetID; Node : NodeID); 
    initial
	start_WS(network_address.net_no, network_address.node_no);
    parallel
        when (?data : Data; ?destination : Address)
            user_conn.to_workstation(?data, ?destination)
        do
            net_conn.to_net(?data, ?destination);
        end;
    ||
        when (?data : Data; ?destination : Address)
            net_conn.to_node(?data, ?destination)
        where ?destination = network_address
        do
            user_conn.to_user(?data);
        end;
end;

type Firewall is interface
-- A firewall is a module with two network connections, one to a LAN
-- the other to a WAN. Conceptually the same as a gateway.
--
--    include  network_node;
    provides        
        network_address : Address;
    service
	net_conn  : network_comm;
-- end include
    service
  	wan_conn : network_comm; 
end;

module newFirewall(address_ : Address) return Firewall is
-- A first approximation to firewall modelling.
-- It passes on to the WAN all messages non-local to the enclosing enclave,
-- and passes onto the LAN all messages on the WAN addressed to this enclave.

        network_address : Address is address_;
    	action start_FW(Net : NetID; Node : NodeID); 
    initial
	start_FW(network_address.net_no, network_address.node_no);
    parallel
        when (?data : Data; ?destination : Address)
            net_conn.to_node(?data, ?destination) 
		where (?destination.net_no /= network_address.net_no)
        do
	-- Here is where we would perform a security check on information
	-- flowing OUT of the enclave
            wan_conn.to_net(?data, ?destination); 
        end;
    ||
        when (?data : Data; ?destination : Address)
            wan_conn.to_node(?data, ?destination)
		where (?destination.net_no = network_address.net_no)
        do
	-- Here is where we could perform a security check on information
	-- flowing INTO the enclave
            net_conn.to_net(?data, ?destination);
        end;
end;