Solution security policy in the ping example
The solution security policy in this example allows you to start all entities, and allows any entity to query the Core and Server entities. Calls to the Server entity are managed by methods of the Flow security model.
The finite-state machine described in the configuration of the request_state Flow security model object has two states: ping_next and pong_next. The initial state is ping_next. Only transitions from ping_next to pong_next and the reverse are allowed.
When the Ping and Pong methods are called, the current state of the request_state object is checked. In the ping_next state, only a Ping call is allowed, in which case the state changes to pong_next. Likewise, in the pong_next state, only a Pong call is allowed, in which case the state changes to ping_next.
Therefore, the Ping and Pong methods can be called only in succession.
security.psl
/* Solution security policy for demonstrating use of the
* Flow security model in the ping example */
/* Include PSL files containing formal representations of
* Base and Flow security models */
use nk.base._
use nk.flow._
/* Create Flow security model object */
policy object request_state : Flow {
type States = "ping_next" | "pong_next"
config = {
states : ["ping_next" , "pong_next"],
initial : "ping_next",
transitions : {
"ping_next" : ["pong_next"],
"pong_next" : ["ping_next"]
}
}
}
/* Startup of all entities is allowed. */
execute {
grant ()
}
/* All requests are allowed. */
request {
grant ()
}
/* All responses are allowed. */
response {
grant ()
}
/* Including EDL files */
use EDL kl.core.Core
use EDL ping.Client
use EDL ping.Server
use EDL Einit
/* When the Server entity is started, initiate this entity with the finite-state machine */
execute dst=ping.Server {
request_state.init {sid: dst_sid}
}
/* When the Ping method is called, verify that the finite-state machine is in the ping_next state.
If it is, allow the Ping method call and switch the finite-state machine to the pong_next state. */
request dst=ping.Server, endpoint=controlimpl.connectionimpl, method=Ping {
request_state.allow {sid: dst_sid, states: ["ping_next"]}
request_state.enter {sid: dst_sid, state: "pong_next"}
}
/* When the Pong method is called, verify that the finite-state machine is in the pong_next state.
If it is, allow the Pong method call and switch the finite-state machine to the ping_next state. */
request dst=ping.Server, endpoint=controlimpl.connectionimpl, method=Pong {
request_state.allow {sid: dst_sid, states: ["pong_next"]}
request_state.enter {sid: dst_sid, state: "ping_next"}
}