Implementing a type system for secure information-flow. Potential security risks

Table of Contents

1 Introduction and Objectives

1.1 Introduction

1.2 Background

1.3 Objectives

1.4 Beneficiaries and personal objectives

1.5 Work plan

1.6 Report structure

2 Context

2.1 Method of literature review

2.2 Compiler functionality

2.2.1 Overview and difference to interpreters

2.2.2 Lexical and syntactic analysis

2.2.3 Semantic analysis

2.3 Terminology of Type

2.3.1 Variables and types

2.3.2 Principal type and principal typing

2.4 Type systems

2.4.1 Important program properties related to type systems

2.4.2 Type rules

2.4.3 Dynamic checking

2.4.4 Subtyping

2.4.5 Flow-sensitive typing

2.4.6 Gradual typing

2.5 Information flow security problem

2.5.1 Security goals

2.5.2 Issues of standard solutions

2.5.3 Security classes

2.5.4 Dynamic and static enforcement mechanisms

2.5.5 Non-interference of information flows

2.5.6 Security type systems and their features

2.5.7 Covert channels

2.5.8 Alternatives to non-interference

3 Methods

3.1 Development methodology

3.2 Development tools

3.3 Software objects that were provided

3.4 Informal description of the While language

3.5 Verification and validation

4 Results

4.1 Selection of type system

4.2 Evolution 1: AST printer and harnessing the visitor pattern

4.3 Evolution 2: AST printer for procedures

4.4 Evolution 3: Dependency map implementation and unit testing

4.5 Evolution 4: Security type system implementation

4.5.1 Flow Principal

4.5.2 Termination Principal

4.6 Evolution 5: Procedure typings

4.6.1 Input parameter dependencies

4.6.2 Output parameter dependencies

4.6.3 Procedure body dependencies

4.6.4 Final typing

4.6.5 Recursive procedure calls

4.7 Evolution 6: Fixed type-checking algorithm

4.8 Evolution 7: Test programs and performance

5 Discussion

5.1 Verification, validation and complexity

5.2 Architectural limitations and alternative designs

5.3 Discussion with attention to real-life scenarios

5.4 Feasibility or impracticability of a security type system for SAP

6 Evaluation, Reflections, and Conclusions

6.1 Project Evaluation

6.2 Further work

Project Goals and Scope

The primary aim of this project is the prototypical implementation of a security type system for a simple While language, designed to statically prevent information leaks at compile-time. The research seeks to demonstrate a reliable and scalable type-checking implementation while investigating the practical feasibility of applying similar security type system concepts to complex enterprise environments like SAP.

• Prototypical implementation of a flow-sensitive security type system.
• Evaluation of type system reliability, performance, and scalability.
• Development of an evolutionary approach for compiler front-end implementation.
• Analysis of architectural limitations and potential for real-life application.
• Investigation into the feasibility of static information flow analysis for SAP ERP systems.

Excerpt from the Book

Summary of Chapters

1 Introduction and Objectives: Introduces the necessity of information flow analysis in modern software and defines the project’s scope and research objectives.

2 Context: Provides the theoretical background regarding compilers, type systems, and the fundamental problems of information flow security.

3 Methods: Details the evolutionary prototyping methodology, development tools, and the language grammar used for testing.

4 Results: Documents the step-by-step implementation of the security type system, including the dependency map and procedure typing algorithms.

5 Discussion: Evaluates the project outcomes, discusses technical limitations, and assesses the feasibility of the proposed system for SAP environments.

6 Evaluation, Reflections, and Conclusions: Summarizes the project experience, provides critical reflection on the process, and suggests directions for future research.

Keywords

information flow analysis, security type system, end-to-end security, confidentiality, non-interference, static analysis, compile-time, flow-sensitive typing, principal types, dependency map, software security, language-based security, While language, procedure typings, termination-sensitivity

Frequently Asked Questions

What is the primary focus of this project?

This project focuses on designing and building a security type system for a simple "While" language to statically enforce confidentiality and prevent illegal information flows at compile-time.

What are the central themes of this research?

The work covers information flow security, the role of security type systems, compiler semantics, static analysis, and the implementation of principal types for procedural programming languages.

What is the core research objective?

The main objective is to implement a reliable and performant security type-checking prototype and to evaluate its scalability and feasibility for potential use in complex enterprise software like SAP.

Which scientific methodology is utilized?

The project employs an evolutionary prototyping approach, building the compiler front-end in iterative phases, which allows for continuous testing and refinement of the type-checking rules.

What does the main body of the report cover?

The main body details the compiler implementation, the design of the dependency map structure (representing variable dependencies), the implementation of type rules (like Assign, Seq, If, While), and the handling of procedure calls.

Which keywords characterize this work?

Key terms include information flow analysis, security type systems, non-interference, principal types, flow-sensitive typing, and static compile-time enforcement.

Why is an immutable "DependencyMap" used in the implementation?

An immutable structure ensures that dependencies are handled deterministically, similar to mathematical functions, which improves reasoning about program state and simplifies the handling of complex matrix operations.

How does the project handle implicit information flows?

The system uses a program counter ("pc") variable that is bound to the entry condition of branch constructs like if-statements and while-loops, ensuring that information dependencies are correctly captured during static analysis.