Secure_PASCAL

Introduction

The Secure Pascal Project is written primarily in C, using bison and flex.

The goal of the project is to demonstrate the mechanics and benefits of automated privilege separation, specifically in the context of Pascal programming. Pascal is the language of choice for this project because of its nature as a strongly-typed language.

The desired functionality is for the user to provide one annotated Pascal program, and receive two unannotated, standard Pascal programs: one “user” and one “privileged” program. The input file is lexed and parsed as an annotated Pascal file, and the resulting AST is used to generate two standard Pascal output files. This process can be broken down into the following steps:

  1. Annotation : The user annotates a standard Pascal program. Using the keywords priv and unpriv, the user may mark individual symbols or a section of code as privileged (or less commonly, explicitly unprivileged). The annotated program must follow standard Pascal syntax, as well as the annotation syntax as specified by the desired security policy level (see below).

  2. Security policy : The user will then execute the Secure Pascal compiler, specifying the annotated input file from Step 1 and the security policy level.

  3. Lexer : The program is lexed.

  4. Parser : The program is parsed within the rules of the appropriate security level. In the case of a syntax error in regards to standard Pascal conventions or annotation syntax, the parser will halt and alert the user.

  5. Code generation : After the parsing step succeeds, the resulting syntax tree will be used by the code generator to produce two standard Pascal output files, and other mechanisms needed to execute the final product. The code generator will separate the statements of the original program according to explicit and implicit privilege level. The result is a privileged and unprivileged program, each written in standard Pascal. Any necessary inter-process communication during runtime for the two programs is accomplished using named pipes. A file will be generated, called run_me.sh, which can create the named pipes, compile the output files fully, and execute them.

  6. Compile output and execute : The two resulting Pascal files, user.pas and priv.pas can be compiled by any standard Pascal compiler, for example FPC, the Free Pascal Compiler. The user can use the file run_me.sh generated by Secure Pascal to fully execute the resulting files, or complete the process manually.

Dependencies

Note: newer versions of GCC do not agree with the flex-generated C files’ formatting. To avoid having to reformat other files, please use gcc 9.5.0 for now.

How to Run

First, create an annotated version of a Pascal program. Specifications for annotated Pascal syntax can be found in the parse documentation.

Run the following command: $bash run.sh <input.pas> <options>

Options

The user may provide a “safe list” of allowed functions to be called in privileged scope. For the lower security policies, STRICT and STRICTER, a safe list is optional. A safe list is compulsory for STRICTEST.

Place the safe list in the inputs directory, named “safelist.txt” with each “safe” function name on a separate line. The program will use this file, if it exists, when parsing.

The user may additionally define a list of “library” functions, or functions available to refence during compilation. These are recognized by the compiler for user-level use. This list must be named “librarylist.txt” in the inputs directory.

If no safe list is defined and the security policy level is STRICT or STRICTER, the privileged component may reference these symbols.

If a safe list is defined, then only the symbols listed in the safe list may be referenced by the privileged component. This means that any symbols listed in the library function list must be listed again in the safe list.

Examples

Sample input programs are provided in the examples directory. Each example has a description that indicates its contents, the necessary security policy, and safe function list if necessary.

Documentation

Lexer Documentation

The lexer is written in flex/lex. Input tokens are identified as TOKENs. More detailed information can be found in the documentation of the lexer files, listed below.

See Lexer Section

Parser Documentation

The parser is written in bison/yacc in C. The parser was built referencing standard Pascal syntax, with some modifications for user annotations.

For more information on parsing rules and formatting requirements for an annotated Pascal input program, see the page below.

See Parser Section

Further Information

Annotations

The Pascal program used as an input to be processed should be annotated by the user. A user may mark a symbol or section of code as priv or unpriv. This explicitly tells the compiler to treat a symbol or section as privileged or unprivileged, respectively.

Appended Syntax Rules

An explicity marked priv symbol or section may not be referenced in an explicitly unpriv or implicitly unprivileged section of code, or be assigned to an unpriviliged symbol.

An exception to this rule is if a user-defined explicilty priv function returns an explicily unpriv result, an unprivileged section or symbol may access this data.

Security Policy Levels

In addition to the modified syntax roles imposed by privilege annotation, the user may specify a security policy level for the parser to follow. The default is strict.

There are four security policy levels:

  1. NONE
    • No cross-privilege restrictions.
    • Privileged data may be accessed from any lower privilege level.
    • Global data may be written or read from any privilege level.
  2. STRICT
    • Privileged data may not be read or written from a lower privilege level. This excludes explicitly unpriv return vaues.
    • Global data may be read or written from any privilege level. This means global variables are shared across the two files.
    • If a file is optionally provided, privileged code may only reference a user-provided list of “safe” functions - all other function calls from privileged sections are disallowed.
  3. STRICTER
    • Privileged data may not be read or written from a lower privilege level. This excludes explicitly unpriv return vaues.
    • Global data may be read from privileged sections of code, but may not be written from privileged sections.
    • If a file is optionally provided, privileged code may only reference a user-provided list of “safe” functions - all other function calls from privileged sections are disallowed.
  4. STRICTEST
    • Privileged data may not be read or written from a lower privilege level. This excludes explicitly unpriv return vaues.
    • Global data may not be read or written from privileged sections or symbols.
    • The user must provide a file that defines a list of “safe” or “allowed” privileged functions. Privileged code may only reference a user-provided list of “safe” functions - all other function calls from privileged sections are disallowed. These “safe” functions may be user defined, in the standard library, or from an arbitrary library.

Code Generation

Output

The complete process will generate three files:

  1. priv.pas : The privileged Pascal program.

  2. user.pas : The user-level Pascal program.

  3. run_me.sh : A script to create the necessary named pipes, compile, and execute the two output programs simultaneously.

If the user executes run_me.sh, the script will create the necessary named pipes, compile the two .pas files, and execute them.