Security

The primary security goal of DkCoder is to allow the script user to assert, before a script is run, whether the script does not access resources like files, the console, sound, etc. Not all scripts can be asserted, but if DkCoder asserts a script does not have access to files for exmaple, then the script does not have access to files under some light assumptions. These assumptions are detailed in this section.

<table class="table"> <caption class="subtitle">Status</caption> <thead> <tr> <th><abbr title="Phase">#</abbr></th> <th>ETA</th> <th>What is Implemented</th> </tr> </thead> <tfoot> <tr> <th><abbr title="Phase">#</abbr></th> <th>ETA</th> <th>What is Implemented</th> </tr> </tfoot> <tbody> <tr> <th>Alpha</th> <td>Now</td> <td>Split the OCaml Standard Library by resource type</td> </tr> <tr> <th>Beta</th> <td>TBD</td> <td>Implementation of the Technical Requirements below</td> </tr> <tr> <th>After GA</th> <td>TBD</td> <td>Allow users to write <a href="https://www.cedarpolicy.com/en">AWS Cedar</a> policies to restrict access to a) resources used by running scripts and b) which scripts can be downloaded and c) data submitted to DkCoder services.</td> </tr> </tbody> </table>

Assumption A1 - A superset of modules used by a script can be obtained

This assumption is based on the OCaml 4.14 environment model Env.t defined in typing/env.mli . These Env.t have values, modules, types, module types, classes and class types produced during compilation. Only add operations like add_value are present, so by the end of compilation we have a superset of statically compiled modules used by the compiled script.

However,

  1. Some of the modules may be functors; that is, new modules can be created at runtime of a specified module type. That leads to a technical requirement:

    If a script uses a functor module, transitively or not, then the script is unassertable (aka. "tainted").

How it will be implemented: The codept analysis tool parses the source and gathers module information, including whether a module is a functor. Using the --log-level DEBUG shows the modules used by the scripts.

Assumption A2 - Access to resources can be gated through modules

By definition, resources are either values like input channels or are accessed through values like function calls (including external C function calls).

In OCaml, values are present in a toplevel Env.t or in a (possibly nested) module and/or class.

  1. Since there is no tool like codept to analyze OCaml classes, there is a technical requirement:

    If a script uses a class, transitively or not, then the script is unassertable (aka. "tainted").

  2. Since the standard OCaml toplevel environment is the contents of the Stdlib module (ie. there is an implicit open Stdlib at the top of each module), and Stdlib contains toplevel values like print_endline, there is a technical requirement:

    All Stdlib toplevel values are annotated with OCaml alerts that fail the compilation when the toplevel values are used.

  3. Since alerts can be locally overridden, there is a technical requirement:

    If a script uses a local alert override, transitively or not, then the script is unassertable (aka. "tainted").

To repeat: In OCaml, values are present in a toplevel Env.t or in a (possibly nested) module and/or class. What remains after implementing the technical requirements above is that resource values necessary for safety assertions are only present in (possibly nested) modules.

How it will be implemented: A PPX can be run that injects a new empty module module Dk__Tainted = struct end whenever a class or local alert override is used. The module analysis by codept will discover the Dk__Tainted, and the analysis phase can fail.

Assumption A3 - Violating the correctness of OCaml type checking can be detected at compile time

The type-safe violations fall into these categories:

  1. Using an external C function declaration
  2. Using the Obj module
  3. Using the Marshal module

This is a weak assumption as it requires expert knowledge of OCaml.

Since the presence of modules can be trivially detected with assumption A1, the technical requirement is:

If a script uses an external C function declaration, transitively or not, then the script is unassertable (aka. "tainted").

How it will be implemented: Any external declaration can be caught by a PPX which injects a module Dk__Tainted = struct end. The presence of any of Dk__Tainted, Obj or Marshal during the codept analysis will taint the script.