Restrictive language semantics in the Multioberon system

IntroductionThe programming language and the Oberon system ^[1] implemented an extremely minimalist approach, in which all functions that are not vital were excluded from the software.

This vector of movement has been preserved in all subsequent implementations of Oberons, which is their significant difference from the generally accepted approach to building software systems, in which the scope of the declared functions is a necessary commercial feature of each new product.

Not only the Oberon project has been developing in the direction of decreasing functionality. Similar approaches are used in the formation of requirements for systems for nuclear power plants performing category A functions ^[2]. This is the highest category in terms of critical software used for reactor protection systems. Category A should guarantee not the presence, but the absence of many standard solutions used by programmers. This software requires the absence of a standard OS and third-party libraries, with the exception of those certified for category A. The requirement of immutability of the run time regardless of the input data leads to the exclusion of cycles with a variable number of iterations and conditional output. The requirement to protect the contents of memory leads to the prohibition of dynamic memory allocation during operation and monitoring. Well-known category A implementations use languages and compilers specialized for these requirements, for example, the language ?C ^[3].

The described approaches demonstrate that requirements significantly affect the software implementation of systems. With stricter requirements, there may be a problem of structural changes in the software. Moreover, with very strict requirements, both the implementation programming language and the compiler may change. This, of course, will not lead to the completion of the existing one, but to the development of a new system.

The author proposes an approach of restrictive semantics, which consists in the following: instead of several languages and compilers, use one language and a compiler frontend with a system of semantic restrictions.

This approach will be described in detail below, as well as the software implementation in the Oberon language in the Multioberon system.

All program examples will be presented in Pascal-like syntax, this development continues the traditions of the Niklaus Wirth school in terms of developing Pascal languages./Modula/Oberon.

The RESTRICT operator as a declaration of restrictions

The mechanism of restrictive semantics is very simple – only the RESTRICT operator is used, declaring a system of restrictions for this software module.

RESTRICT -, -*, +, ..;

where - represents some token, which the compiler interprets as an additional restriction for this module (the ‘-‘ sign means to exclude the token). In turn, + represents the inclusion of existing functionality that is excluded by default. The scope of the restriction is a software module. Oberon is a modular programming language, where a module is located in a single file and is a unit of compilation, loading and execution. Therefore, the restrictions apply only to this software module. If it is necessary to distribute the restriction system to several software modules, then a restriction file with an external scope (the ‘*’ sign) is created, which must be imported into each software module. For example, the IMPORT RestrictIEC880 operator imports all restrictions recorded in the RestrictIEC880 module as external. For example, if RESTRICT –WHILE*, -LOOP* are written in it, this will prohibit the use of WHILE, LOOP operators.

If the module code does not comply with the restriction system, semantic analysis should not take place, and, as a result, a compilation error is issued.

Limiting the number of iterations of the loop

For example, a requirement to limit the number of iterations of the cycle is imposed on the developed real-time application system. In the standard ^[2], this is formulated as "the run time should not change significantly as a result of changing the input data." This means that the text of the program being developed should contain only FOR loops with a constant number of iterations. Therefore, the compiled binary code of this module will also be with a fixed number of iterations, regardless of the configuration or conditions for running this code. Restrictive semantics in terms of constant iterations of the loop will mean the prohibition of other types of loops.

RESTRICT –WHILE, -REPEAT, -UNTIL, -LOOP;

As a result, only the FOR j loop will remain := 1 TO N-1 DO .. END, which has a constant number of iterations N, regardless of external conditions. But even for the FOR loop, there are a number of cases when the parameter N may depend on external conditions. This can lead to varying run times. In this case, you should limit the use of the limits of the FOR loop to constants, i.e. prohibit variables for limits.

RESTRICT –FOR(VAR);

The compiler's handling of this limitation requires a level of semantic analysis. Unlike prohibiting a keyword (for example, WHILE) entirely, excluding the limits of loop variables leads to the need to analyze the syntax tree ^[4] taking into account semantic information about types. Figure 1 illustrates a tree for performing such an analysis.

Fig. 1. Abstract syntax tree of the FOR loop

Fig.1 Abstract Syntax Tree of FOR cycle

When the –FOR(VAR) constraint is set, the compiler must activate checks of the FOR->COND->N limit token with this constraint. Since the limit token in the figure is a variable, the check fails, and the compiler issues an error message.

The run time of a module may also depend on the run time of procedures of other imported modules. For example, there may be such a call to the OtherModule procedure.LongCalculations(). This means that in the OtherModule module, the requirements for limiting the number of iterations of loops may not be met. Therefore, the OtherModule module should be considered in the same way. If semantic restrictions on the module are not set, then there is no confirmed declaration of compliance with the requirements.

Dynamic Memory limitation

The paper ^[5] shows how the properties of a computer system in terms of memory can degrade over time, and that an important criterion is ergodicity, i.e. the stability of these properties, which requires evidence, including architectural nature. It also shows that it is necessary to proceed from the presumption of non-ergodicity, i.e. to assume that the characteristics of the software being developed may degrade over time. The system of semantic constraints serves as a good tool for such proof of ergodicity.

For many real-time systems, a ban on dynamic memory allocation is needed. Inside the module, this is done by limiting the built-in NEW function.

RESTRICT –NEW;

This means that the NEW function cannot be called directly in this module. In this case, the allocation of dynamic memory can be caused by a function from another, imported module, for example, Factory Factory.New(). In addition to considering the limitations of the imported module, you can prohibit the use of pointers.

RESTRICT –NEW, -POINTER;

Then the check will not be passed and will end with a syntax error.

VAR ptr: POINTER TO FactoryElem;

ptr := Factory.NewElem;

The next way to circumvent the restriction is to use the library functions malloc, calloc, strdup, etc. These functions return an untagged pointer to memory, which can then be converted into a pointer used in Oberon using the SYSTEM module. To exclude such pointers, it requires prohibiting the use of the SYSTEM module.

RESTRICT –NEW, -POINTER, -SYSTEM;

The final condition for limiting the dynamic memory of the module will have all three components.

Stack Memory Limitation

In Oberon systems, stack memory is fixed for each process and cannot be increased subsequently. Going beyond the limits of stack memory can occur with deep recursion in the software used. The consequence of going out of bounds is a fatal memory error. This must be avoided. The prohibition of using recursion looks like this.

RESTRICT –PROCEDURE(PROCEDURE);

With the established restriction -PROCEDURE(PROCEDURE), the syntax tree is analyzed to identify recursions. The identified cases lead to a syntax error.

A way to circumvent these restrictions may be to force the installation of a stack pointer through register operations, for example, SYSTEM.PUTREG(SP, address). To avoid this, you need to disable the PUTREG function that works directly with registers.

Another way to circumvent the restriction would be to use the library function alloca or similar. The method of struggle will also be the prohibition of the SYSTEM.

RESTRICT –PROCEDURE(PROCEDURE), -SYSTEM;

Using guarantees of stack memory limitations has practical benefits. The author faced a situation when it was necessary to organize a quick sorting of dynamically incoming signals in a soft real-time system. A rare situation was discovered that during a peak signal flow, the quick sort program crashed due to going beyond the boundaries of stack memory. As a result, a non-recursive quick sort algorithm was found and implemented ^[6], which subsequently showed its stable operation. If there were 2 modules developed, one without restrictions, and the second with the prohibition of recursion, then the choice would be unambiguous in favor of option 2.

Buffer Overflow Attacks

The buffer overflow attack is an attack on the most common vulnerability in the field of software security ^[7]. The authors ^[7] recommend "paying attention to languages that provide type checking and preservation, as in Java, excluding buffer overflow. However, we should not forget that the Java Virtual Machine is written in C and, thus, may have vulnerabilities."

Oberon is a statically hard-typed system. The Oberon runtime environment is written in Oberon, which is a statically typed language. Therefore, on a pure Oberon, an attack on buffer overflow is impossible, since copy operations are performed between hard-typed objects with a fixed length.

However, there is a SYSTEM module that declares the use of low-level system operations. For example, when using it, you can copy using addresses and lengths.

SYSTEM.MOVE(srcAddr, dstAddr, length);

In addition, SYSTEM.PUT(addr, value) procedures can record information at an arbitrary address, for example, change the return address or a pointer to a function. There is another way – to get the address of the stack and work with it as with an array of pointers.

rawAddr := SYSTEM.ADR(localVar); rawAdr[16 (* offset *)] := x;

The way to deal with vulnerabilities in the form of buffer overflow will be, at a minimum, the prohibition of these functions.

RESTRICT -MOVE, -PUT, -ADR;

A more accurate solution would be to ban the SYSTEM module.

RESTRICT -SYSTEM;

It should be noted that using commands from SYSTEM in the standard Oberon requires an explicit declaration of importing this module.

IMPORT SYSTEM;

Such a declaration clearly indicates the need to use potentially unsafe functions (in the sense of type safety) in the software module being developed. If the developer has specified the SYSTEM import, then he declares potentially vulnerable places. If there is a restriction on the use of SYSTEM (for example, by importing a module with RESTRICT -SYSTEM), then this leads to a syntax error during compilation.

Of course, this vulnerability will be caused by using the functions of the standard library memcpy, strcpy, working with untagged pointers. However, working with these pointers is possible only when using the SYSTEM module.

The problem of a fragile base class

The problem of a fragile base class ^[8] is hidden dependencies when inheriting a non-abstract class by third-party developers. Consider such a base class that has an implementation of the inc2 method. This implementation is inherited, which is defined by the EXTENSIBLE keyword.

TYPE Base = EXTENSIBLE RECORD counter: INTEGER END;

PROCEDURE (VAR b: Base) inc2(), NEW, EXTENSIBLE;

BEGIN INC(b.counter) END inc2;

PROCEDURE (VAR b: Base) inc1(), NEW; BEGIN b.inc2 END inc1;

A derived class, knowing only the interface of the base class, can offer its own implementation of inc2.

TYPE Ext = RECORD (B.Base) END;

PROCEDURE (VAR e: Ext) inc2(); BEGIN e.inc1 END inc2;

Such an outwardly correct construction will lead to the appearance of an infinite recursion, inc1->inc2->inc1.

The problem with this example and the fragile base class is implementation inheritance. In Oberon (hereafter the dialect Oberon-CP is used, sometimes referred to by the commercial name Component Pascal, Eng. Component Pascal, https://blackboxframework.org/index.php?cID=home-ru ,ru,) implementation inheritance is explicitly marked with the EXTENSIBLE keyword. If the procedure is EXTENSIBLE, then this indicates the inheritance of the implementation. The use of EXTENSIBLE, as well as SYSTEM, is a declaration of subsequent violations of the normal order of things in the program code. In other languages, for example, Java, the keyword final was not quite successfully introduced for these purposes, the absence of which occurs when the class system is abnormally designed.

The declaration prohibiting inheritance of an implementation looks like

RESTRICT -EXTENSIBLE;

This ensures that there is no fragile base class problem for the types of the entire module. Such a successful, in comparison with Java, the syntax of Oberon allows you to simply ban the keyword, and not to build complex semantic schemes of checks.

The problem of nested procedures

Nested procedures are located inside other procedures and have access to their local variables. The problem of nested procedures ^[9] occurs when leaving the scope of the parent frame, which is illustrated by the following code.

VAR vProc = PROCEDURE(val: INTEGER);

PROCEDURE Parent();

   VAR loc_val: INTEGER;

   PROCEDURE Child(val: INTEGER);

   BEGIN loc_val := val END Child;

BEGIN Child(12);

   vProc := Child;

   vProc(13)     (* --- CRASH --- *)

END Parent;

Assigning the Child procedure address to the vProc global variable is not prohibited. But activating this procedure vProc(13) leads to an execution error due to the lack of correct access to the stack of the Parent procedure.

The way to solve this problem is to prohibit the use of local procedures, defined as

RESTRICT –BEGIN(PROCEDURE);

With this prohibition, the procedure of the example above will move to the global scope with the prototype PROCEDURE Child(val: INTEGER; VAR loc_val: INTEGER), in which the output parameter will be added.

The problem of the WITH operator

The problem with the WITH operator is that it simultaneously implements the functionality of a switch and a type change. This leads to code ambiguity and ambiguity in the compilation verification mechanisms. Consider the following example.

TYPE Base = POINTER TO ABSTRACT RECORD END;

Ext1 = POINTER TO RECORD (Base) END;

Ext2 = POINTER TO RECORD (Base) END;

VAR vBase: Base;

vExt2: Ext2;

WITH vBase: Ext1 DO       (* vBase IS Ext1 *)

   vBase := vExt2          (* vBase IS Ext2 *)

END;

vBase := vExt2;           (* vBase IS Ext2 – Possible? *)

In this example, the variable vBase is treated as a pointer to the Base type before entering the WITH scope, and after entering it is treated as a pointer to the Ext1 type. Therefore, assignment outside of the WITH scope is acceptable, but not inside.

The solution is to ban WITH.

RESTRICT –WITH;

In this case, you can use the IS type check operator and enter local variables of Ext1, Ext2 types with explicit conversion of ext1 types := vBase(Ext1).

Extensibility of the language syntax

The above lexemes of the RESTRICT operator worked towards limiting functionality. However, this operator allows you to reactivate the functionality disabled by default.

For example, when switching from 32 to 64 bits, it was necessary to enter an integer type with the size of an address, 4 bytes for 32-bit environments and 8 bytes for 64-bit ones. The compiler was extended with the ADRINT type, but since this type was not included in the language message, it became deactivated by default. You can reactivate it with the RESTRICT operation.

RESTRICT +ADRINT;

VAR ai: ADRINT;

ai := SYSTEM.VAL(ADRINT, Api.GetAddr());

This number stores the integer address obtained from the pointer returned by Api.GetAddr().

Programming languages also evolve over time. However, when switching to new versions, there is often a discontinuation of support for old ones. For example, Python 2.7 has been discontinued since 2020 (https://legacy.python.org/dev/peps/pep-0373 / ).

Instead of expanding and changing versions of the syntax of the language, it is proposed using the mechanism of restrictive semantics to use a step-by-step explicitly declared extension by adding new keywords. The RESTRICT +ADRINT declaration adds a new keyword and ADRINT type. The expansion of the programming language due to new keywords and concepts cannot happen indefinitely. This path is a dead end. Therefore, expansion is allowed due to a very limited number of keywords.

Dynamics of dialect development, Oberon-07/13/16

Oberon from the author developed dynamically, the dialects of Oberon from 2007, 2013 and clarifications in the 2016 version were created. The development went mainly towards the exclusion of non-necessary functionality ^[10].

The main changes in the language are summarized by the author in the table in Figure 2.

Fig. 2. N.Wirth's changes in the Oberon language

Fig 2. N.Wirths changes in Oberon language

The analysis of the above changes shows that 9 out of 12 changes represent prohibitions on the use of certain syntactic and semantic constructions in the language. For example, to fulfill clause 6 (the RETURN statement can only be at the end of a function that returns a value), you need to add a semantic constraint.

RESTRICT –RETURN(PROCEDURE);

This will allow you to make the appropriate check on the nodes of the syntax tree.

At the same time, 3 out of 12 changes entail a change in the syntax of the ELSE(WHILE), CASE, PROCEDURE statements. The change of the CASE operator is due to the fact that the type checking operation passes from the WITH operator to the CASE operator, at the same time, type conversion is excluded along with the WITH operator. The remaining changes add additional functionality. For these changes, it is necessary to define tokens and provide for their activation in the compiler, a possible option is given.

RESTRICT +ELSE(WHILE), +CASE(POINTER), +PROCEDURE(SYSTEM);

If there is support for new modified syntactic constructions, then you can build a compiler for the 07/13/16 dialect.

Based on the results of the evaluation of the changes made to Oberon 07/13/16, it can be concluded that potentially problematic places have been excluded. Among them are WITH with variable type conversion, LOOP loop with an implicitly defined exit condition, exclusion of ambiguity when casting integer and real types, return of a value at the end of the procedure, etc. Exclusion of problematic places minimizes the possibility of writing problematic code, which, in turn, will make it possible to assert an increase in software reliability.

Features of the compiler implementation

The extensibility and limitability properties inherent in the system dictate the structure of the implementation of a compiler that meets these requirements. In conditions of such variability, the solution with the separation of the frontend and backend seems to be the best^[11]. The frontend builds a syntax tree, the backend performs code generation to the target platform.

The approach with restrictive semantics proposed in the introduction suggests using one language and compiler instead of several. At the same time, it should be noted that for different environments there may be different and substantially different backends. Binary codes for ARM firmware will differ significantly from Windows software, and LLVM bytecode will differ from Java Virtual Machine bytecode.

As part of the implementation of the proposed approach, a Multioberon compiler with a set of replaceable backends was developed.

Fig. 3. Multi-compiler with a set of backends

Fig.3. Multi-compiler with a set of backends

The concept of a universal frontend for the development of a ported OP2 compiler was proposed in ^[12] and received several software implementations.

The implementation of the Oberon-CP dialect in the form of a system built on the basis of component software was carried out in the BlackBox Component Builder system ^[13]. The compiler of the specified system has been redesigned and connected to the Multioberon as a replaceable Omb backend. Built on the basis of OP2, the frontend of the BlackBox system has been redesigned and formed the basis of the Multioberon frontend.

Another OP2-based compiler Offront (https://github.com/jtempl/ofront ) creates the output code in the C language . He clarifies the system of checking the correctness of pointer types in comparison with the basic one in OP2 ^[14]. Offront has been substantially modified and connected to the system as an Omf backend.

The Oml backend, which has an LLVM byte code at the output, was fully developed by the author for the Multioberon system.

It is supposed to be possible to expand backends for target platforms.

At the output of the frontend, an AST syntax tree, a Sym Tab symbol table and a set of used RESTRICT constraints are created. The set of restrictions used must correspond to the capabilities of the backend. If there is no such match, then an error is generated during compilation.

The entire Multioberon system with replaceable backends is available at https://github.com/dvdagaev/Mob . The current version 1.2 supports X86, X64, ARM32, Aarch64 architectures for Linux, Windows, Raspberry Pi OS.

Example of compiler operation

An example of analysis by a compiler with set restrictions from the BlackBox graphics system is shown in Figure 4.

Fig. 4. Listing with violations of restrictions

Fig.4. Listing with restrictions violations

This listing shows that, despite the established restriction on the use of nested procedures –BEGIN(PROCEDURE), procedure One is located inside the parent Fact. The consequence of this is the syntax error "nested procedure is not allowed". In addition, despite the established restriction –RETURN(PROCEDURE), the Fact function implements a return from the middle of the code. The consequence of this is the syntax error "unexpected RETURN position". And finally, despite the limitation of using recursion –PROCEDURE(PROCEDURE), the Fact function is designed to be recursive. The consequence of this is the syntax error "recursion is not allowed".

Multioberon scaling/demoscaling strategy

The proposed implementation of the Multioberon system at this stage represents a reference level in terms of functionality. At the same time, it is possible to reduce functionality due to additional restrictions, as well as a limited increase in functionality. Figure 5 illustrates the directions of development.

Fig. 5. Scaling/demoscaling of the Multioberon

Fig.5. MultiOberon scaling up and down

Oberon-CP is a reference level that does not require setting limits. When switching to the functionality of Oberon-07, it is necessary to use a system of restrictions, while getting a more definite picture in managing the types and flow of the program (flow control, no type changing). The introduction of additional restrictions to Oberon 07 in order to comply with the IEC880 standard will require the prohibition of dynamic memory and the variability of the execution of cycles (runtime variation, dynamic memory). This will mean demoscaling. When demoscaling (the downward movement in the figure), the number of constraints increases, and the number of functions decreases. At the same time, the number of vulnerabilities decreases and reliability increases.

Scaling from the reference level means the explicit introduction of additional functions, for example, the introduction of active objects of the Active Oberon language ^[15]. The backend used must support these additionally entered functions.

ADA Language Restriction System

When designing the constraint system, the experience of the Ada GNAT compiler in creating constraints was taken into account (https://docs.adacore.com/gnat_rm-docs/html/gnat_rm/gnat_rm/standard_and_implementation_defined_restrictions.html ). The Ada approach focuses on the use of a number of semantic checks (recursion, dynamic memory allocation) and a large number of settings of the executing system. High reliability of Ada is achieved due to redundancy of software solutions.

The Multioberon approach is aimed at expanding and demoscaling the capabilities of the Oberon language itself. The high reliability of Oberon is achieved due to the minimalism of the software solutions used.

Conclusion

The approach of restrictive semantics proposed in this article allows you to choose a set of minimum necessary tools for solving problems with a different scale of requirements. For mission-critical systems and requirements, it is necessary to develop code with a maximum system of restrictions. For real-time tasks, it is necessary to abandon solutions that potentially block the execution flow.

Guarantees of compliance with the requirements of restrictive semantics are provided on the basis of syntactic and semantic analysis of programs during development, and not by subsequent expert means of code analysis for vulnerability. Compliance of the module with the system of restrictions is a prerequisite for successful compilation of the program.

The "from constraints" approach involves declaring compliance with the necessary design requirements to developers. Conversely, the rejection of restrictions implies a complete non-compliance with the system of requirements.

In the construction of ergodic systems, the rejection of constraints means the rejection of the proof of ergodicity. This practice is not generally accepted. However, given the presumption of non-ergodicity, it is postulated that the characteristics of the software being developed degrade over time. And if there are no restrictions on the use of dynamic memory in the software, then it will be used according to the worst scenario of those that the OS kernel and the swapping system will allow.

The general rule of construction: the more restrictions on the use of software, the more reliable and predictable this software will be.