ATLAS

Overview

ATLAS generates ACSL annotations from a dedicated formal specification language for access control policies.

This language allows for modeling an access control policy, and linking it to a C source code. Plug-in WP (deductive verification) or E-ACSL (runtime annotation checking) can then be used to verify the generated ACSL annotations on the source code: If so, it means that the source code correctly implements the modeled access control policy.

Usage

Here is a minimal example of an access control policy for a thread manager that should enforce two rules:

• Rule 1. A process can only be killed by the process that has created it.
• Rule 2. After being killed, a process does not exist anymore.

These rules are modeled in file spec.atl:

/* ------------------ */
/* Type declarations */
/* ------------------ */

/* Link generic access control notions to C types */
type SUBJECT = pid_t;
type OBJECT = pid_t;
type RIGHT = enum right {'create', 'delete'};

/* -------------------- */
/* Command declarations */
/* -------------------- */

/* Define a new command updating the access control model
   when killing a thread */
kill_child_cmd(SUBJECT parent, SUBJECT pid)
{ /* command preconditions */
  sbj_defined(parent) &&
  obj_defined(`OBJECT`(pid)) &&
  check_entry(parent, `OBJECT`(pid), delete);
}
{ /* command actions in terms of access control effects */
  rm_subject(pid);
  rm_object(`OBJECT`(pid));
}

/* -------------------- */
/* Linking instructions */
/* -------------------- */

/* the rules must be enforced at Line L of function kill_child in the C file */
void kill_child(pid)@L = kill_child_cmd(current_pid, pid);

You can generate the ACSL annotations from this model for some input C files by running:

$ frama-c -atlas -atlas-spec=spec.atl input_file.c -print -ocode annot_file.c

Then, you can use either WP or E-ACSL in a standard way to verify the generated file.