The basic scenario for using the Policy Assertion Language (PAL) is to create test scenarios for checking solution security policies written in PSL.
The PAL language lets you generate and send requests to the security module and verify that the received decisions comply with the expected decisions. To run test scenarios written in PAL, you do not need to generate code of client-server interactions because PAL operates at the level of abstraction of the security module.
General syntax
A test scenario is a sequence of requests to the security module, with an expected decision indicated for each of these requests.
Test scenarios can be combined into groups. A group of scenarios may also contain the setup and finally sections, which will be executed before and after the execution of each scenario in this group, respectively. This can be used to define common start conditions or to check common invariants.
The modular assert declaration is used to declare a group of test scenarios:
assert "scenario group name" {
setup {}
sequence "name of scenario 1" {}
sequence "name of scenario 2" {}
...
finally {}
}
Syntax of requests
To configure requests within test scenarios, the following types of declarations are used:
<expectation> <header> <operation> <event selectors> {message}
In this case:
<expectation> – expected decision: grant, deny or any. When expecting the any decision, the decision of the security module is ignored, but an error when completing the request will mark the test scenario as unsuccessful.
When the expected decision is not explicitly indicated, the grant decision is expected.
<title> – optional parameter containing a text header of the described request.<operation> – one of the types of queries to the security module: execute, security, request or response.<event selectors> – the permissible selectors of an event coincide with the selectors used when binding methods of security models to security events. For example, you can indicate the message recipient entity or the called method.{message} – optional parameter containing the value for arguments of the called method. The value of this parameter must match the operation and selectors of the request. An empty number of arguments {} is used by default.Example:
assert "some tests" {
sequence "first sequence" {
// When the Client entity calls the Ping method of the pingComp.pingImpl interface implementation of the Server entity, the grant decision is expected
// In this case, the value 100 is passed in the value argument of the Ping method
grant "Client calls Ping" request src=Client dst=Server endpoint=pingComp.pingImpl method=Ping {value: 100}
// It is expected that the Server entity is denied from responding to requests of the Client entity
deny "Server cannot respond" response src=Server dst=Client
}
}
Abbreviated format of requests
For convenience, you can also use the following abbreviated formats of requests:
execute operation, you can save the handle of the started entity to a variable by using the <- operator.security operation: <entity> ! <path.to.method> {message}When executed, it is expanded to the full format: security src=<entity> method=<path.to.method> {message}
request operation: <client> ~> <server> : <path.to.method.implementation> {message}When executed, it is expanded to the full format: request src=<client> dst=<server> endpoint=<path.to.implementation> method=<method> {message}
response operation: <client> <~ <server> : <path.to.method.implementation> {message}When executed, it is expanded to the full format: response src=<server> dst=<client> endpoint=<path.to.implementation> method=<method> {message}
Example:
assert "ping test"{
setup {
// variable s contains a pointer to the running instance of the Server entity
s <- execute dst=ping.Server
// variable c contains a pointer to the running instance of the Client entity
c <- execute dst=ping.Client
}
sequence "ping ping is denied" {
// When the Client entity calls the Ping method of the pingComp.pingImpl interface implementation of the Server entity, the grant decision is expected
// In this case, the value 100 is passed in the value argument of the Ping method
c ~> s : pingComp.pingImpl.Ping {value: 100 }
// The deny decision is expected when the call is repeated
deny c ~> s : pingComp.pingImpl.Ping {value: 100 }
}
sequence "normal" {
// Grant decisions are expected when the Ping and Pong methods are sequentially called
c ~> s : pingComp.pingImpl.Ping { value: 100 }
c ~> s : pingComp.pingImpl.Pong { value: 100 }
}
}
Running tests
To run test scenarios written in PAL, use the --tests run flag when starting the nk-psl-gen-c compiler:
$ nk-psl-gen-c --tests run <other parameters> ./security.psl
The nk-psl-gen-c compiler generates code of the security module and code of test scenarios, uses gcc to compile them, and then runs them.
To generate code of test scenarios without compiling and running them, use the --tests generate flag.