Including PSL files
To include a PSL file, use the following declaration:
use <link to PSL file._>
The link to the PSL file is the file path (without the extension and dot before it) relative to the directory that is included in the set of directories where the nk-psl-gen-c compiler searches for PSL-, IDL-, CDL-, and EDL files. (This set of directories is defined by parameters of the makekss script in the format "-I <path to files>".) A dot is used as a separator in a path description. A declaration is ended by the ._ character sequence.
Example:
use policy_parts.flow_part._
This declaration includes the flow_part.psl file, which is located in the policy_parts directory. The policy_parts directory must reside in one of the directories where the nk-psl-gen-c compiler searches for PSL-, IDL-, CDL-, and EDL files. For example, the policy_parts directory may reside in the same directory as the PSL file containing this declaration.
Including a PSL file containing a formal representation of a security model
To use the methods of a required security model, include a PSL file containing a formal representation of this model. PSL files containing formal representations of security models are located in the <KOS_KASPERSKY> SDK at the following path:
toolchain/include/nk
Example:
/* Include the base.psl file containing a formal representation of the
* Base security model */
use nk.base._
/* Include the flow.psl file containing a formal representation of the
* Flow security model */
use nk.flow._
/* The nk-psl-gen-c compiler must be configured to search for
* PSL-, IDL-, CDL-, and EDL files in the toolchain/include directory. */