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 the parameters -I <path to files> when starting the makekss script or the nk-psl-gen-c compiler.) 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 description of a security model

To use the methods of a required security model, you need to include a PSL file containing a formal description of this model. PSL files containing formal descriptions of security models are located in the KasperskyOS SDK at the following path:

toolchain/include/nk

Example:

/* Include the base.psl file containing a formal description of the

* Base security model */

use nk.base._

/* Include the flow.psl file containing a formal description 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. */