security.psl

/**
 * © 2025 AO Kaspersky Lab
 * Licensed under the MIT License
 */

/* Description of a solution security policy. */

/* Include the base.psl file containing a formal description of the Base security model. */
use nk.base._

/* Include EDL files. */
use EDL Einit
use EDL kl.core.Core

/* EDL descriptions of Consumer and Producer. */
use EDL protobuf_example.Consumer
use EDL protobuf_example.Producer

{% if BOARD == "RPI4_BCM2711" %}
use kl.drivers.Bcm2711MboxArmToVc._
{% elif BOARD == "RADXA_ROCK_3A" %}
use kl.drivers.PinCtrl._
use kl.drivers.GPIO._
{% endif %}
use kl.EntropyEntity._
use kl.core.DCM._
use kl.drivers.BSP._
use kl.VfsSdCardFs._
use kl.drivers.SDCard._
use kl.bc.BlobContainer._
use logrr.Server._
use logrr.FsOutputChannel._

/* Assign the execute interface. */
execute: kl.core.Execute

execute {
    /* The KasperskyOS kernel is allowed to start itself and the Einit class process. */
    match src = kl.core.Core {
        match dst = kl.core.Core                  { grant () }
        match dst = Einit                         { grant () }
    }

    /* The Einit class process is allowed to start specific processes. */
    match src = Einit {
{% if BOARD == "RPI4_BCM2711" %}
        match dst = kl.drivers.Bcm2711MboxArmToVc { grant () }
{% elif BOARD == "RADXA_ROCK_3A" %}
        match dst = kl.drivers.PinCtrl            { grant () }
        match dst = kl.drivers.GPIO               { grant () }
{% endif %}
        match dst = kl.VfsSdCardFs                { grant () }
        match dst = kl.drivers.SDCard             { grant () }
        match dst = kl.EntropyEntity              { grant () }
        match dst = kl.core.DCM                   { grant () }
        match dst = kl.drivers.BSP                { grant () }
        match dst = kl.bc.BlobContainer           { grant () }
        match dst = logrr.Server                  { grant () }
        match dst = logrr.FsOutputChannel         { grant () }
        match dst = protobuf_example.Consumer     { grant () }
        match dst = protobuf_example.Producer     { grant () }
    }
}

request {
    /* The specified clients are allowed to query the KasperskyOS kernel. */
    match dst = kl.core.Core {
        match src = Einit                     { grant () }
        match src = logrr.Server              { grant () }
        match src = logrr.FsOutputChannel     { grant () }
        match src = protobuf_example.Consumer { grant () }
        match src = protobuf_example.Producer { grant () }
    }

    /* The specified clients are allowed to query a server of the kl.core.DCM class. */
    match dst = kl.core.DCM {
        match src = logrr.Server                    { grant () }
        match src = logrr.FsOutputChannel           { grant () }
    }

    /* The specified clients are allowed to query a server of the kl.VfsSdCardFs class. */
    match dst = kl.VfsSdCardFs {
        match src = kl.bc.BlobContainer       { grant () }
        match src = logrr.Server              { grant () }
        match src = logrr.FsOutputChannel     { grant () }
        match src = protobuf_example.Producer { grant () }
    }

    /* Any client and the KasperskyOS kernel are allowed to query a server of the
     * kl.bc.BlobContainer class. */
    match dst = kl.bc.BlobContainer {
        grant ()
    }

    /* The specified clients are allowed to query a server of the logrr.Server class. */
    match dst = logrr.Server {
        match src = logrr.FsOutputChannel     { grant () }
        match src = protobuf_example.Consumer { grant () }
        match src = protobuf_example.Producer { grant () }
    }

    /* The client of the protobuf_example.Producer class is allowed to query a server of the
     * protobuf_example.Consumer class. */
    match dst = protobuf_example.Consumer {
        match src = protobuf_example.Producer { grant () }
    }
}

/* Any server and the KasperskyOS kernel are allowed to respond to queries of any client. */
response {
    grant ()
}

/* Any server and the KasperskyOS kernel are allowed to notify any client regarding errors that
 * occur when the client queries the server or the kernel by calling any method. */
error {
    grant ()
}