The objectives of this project are to design, implement and systematically demonstrate a chosen type system considering reliability, performance, and scalability. Furthermore, it aims to determine the limitations of the implementation and alternative architectural designs, to evaluate the extent to which the developed prototype scales up to real-life scenarios and to investigate the feasibility of a similar security type system for SAP systems.
Standard security practices, such as access controls, insufficiently assure secure end-to-end behaviour of an application. Any program flaw, no matter how small or big, poses a potential security risk. Static information flow analysis checks a program for confidential information leaks into public data containers at compile-time.
This design-and-build project’s aim is the prototypical implementation of a security type system for a simple demonstrative language to prevent programs leaking confidential information effectively. The project is based on existing research concerning security type systems as a means of enforcing information flow policies in a program. The results are discussed not only in terms of validity but also considering the feasibility of a similar security type system for SAP enterprise resource management systems.
Society relies heavily on software-intensive systems in all facets of life. Information is automatically processed in automobiles, phones, fridges, and countless web servers. Much of that information is personal data and can distinguish an individual’s identity, such as their name, biometric records, or email addresses. Intellectual property and confidential information are handled in mission-critical military, governmental, medical and business applications. Therefore, building trust in the handling of data by systems is a crucial aspect of software architecture design.
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
4.5.1 Flow Principal
The security type system (class SecurityTypeSystem) has an instance attribute allVariables which contains all program variables, naturally without duplicates. This set can be empty as While programs can be well-formed without program variables in one case, namely when they only contain procedure calls and empty procedure definitions. The Skip type rule does not need to be implemented since the keyword skip is not part of the language. Skip is normally useful for specifying unambiguous language constructs. For instance, in the conditional if E then C else skip, the else branch is necessary to prevent the ambiguous syntax if E1 if E2 then C1 else C2.
The Assign type rule derives a dependency of a variable v on the left-hand side of the operator on all program variables contained in the expression on the right-hand side. In addition, v becomes dependent on the program counter. If a variable is not dependent on pc in the final program typing, it was never assigned. The implementation of the visitor method in Listing 10 for assignment illustrates how the type-checker works.
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.
- Arbeit zitieren
- Dominik Kropp (Autor:in), 2019, Implementing a type system for secure information-flow. Potential security risks, München, GRIN Verlag, https://www.grin.com/document/962215
