s196671 Josefine Rosalie Balch Petersen
s204683 Adrian Zvizdenco 𝓩𝓮𝓭𝓻𝓲𝓬𝓱𝓾
s204708 Jeppe Moeller Mikkelsen
It is absolutely necessary to have fsyacc and fslexx installed to run the GCL-parser If not installed follow the instructions
Inputs to terminal:
- dotnet fsi MainProject.fsx
- Menu of options appear
When running the code a menu should pop-up with the options specified below.
The input files potentially used are located in the FilesIN folder and can be edited there, while the output files are going to be updated in the FilesOUT folder.
1. Pretty Printer
2. Non-Deterministic Program Environments
3. Deterministic Program Environments
4. Security Analysis
5. Exit Menu
After choosing an option, the input should be of Dijkstra's Guarded Command Language (possibly with annotations). The tool provides 2 methods to input the program - one from a txt file (Input.txt or Program.txt) and one from the console:
Choose input source:
1. Text file ('___.txt')
2. Console
If the input is not a valid GCL, the parser will acknowledge and send the user a special error message and tell where the error has been found, as in the following example.
Parse error at : Line 1, 6, Unexpected token: :=
When choosing either a Non-Deterministic Program Graph or a Deterministic Program Graph, the program graph will be constructed. Afterwards the following extended menu will be given:
1. Step-wise Execution with Automatic Input
2. Step-wise Execution with User Input
3. Program Verification
4. Program Sign Analysis
5. Model Checking
6. Return to main menu
This extended menu gives the user the option of seeing a step-wise execution with either automated-input or with user-input for variables and arrays, perform a program verification or simply return to the main menu as given above.
These commands represent an extended set of Dijkstra's Guarded Commands Language syntactics
| Expressions | Description |
|---|---|
| Arithmetics a : := | n | x | A[a] | a + a | a - a | a * a | a / a | - a | a ^ a | (a) | ln a | log a |
| Boolean b : := | true | false | b & b | b | b | b && b | b || b | !b | a = a | a != a | a > a | a >= a | a < a | a <= a | (b) |
| Commands C : := | x := a | A[a] := a | skip | C ; C | if GC fi | do GC od | do [P] GC od |
| Guarded Commands GC : := | b -> C | GC [] GC |
| Predicates P: := | true | false | x | P ∨ P | P ∧ P | ¬P | P => P | a = a | a != a | a > a | a >= a | a < a | a <= a | (P) |
| Annotations AN: := | begin [P] C end [P] | C end [P] | begin [P] C | C |
If commands not understood, a reference can be found here
Exceptions to be aware of:
Skip should have two spaces after input |skip--|, hyphens are in these case supposed to be spaces.
If one doesn't annotate the program, but chooses to perform a program verification, all predicates are going to be initialized to the value true.
After each of the annotating tags (begin | end) there is a whitespace to delimit the predicate in brackets.
The Program Graphs are developed by two main functions:
- Generate Deterministic Program Graphs
- Generate Non-Deterministic Program Graphs
These function takes the expressions and turn them into a list of edges containing (node(int), expression(command), node(int)).
These lists are of course different, depending on the choice of the desired Program Graph. The differences in syntax for the Non- and Deterministic Program Graphs can be seen in the book Formal Methods chap. 2 from Course 02141 - Computer Science Modelling on DTU.
In order to generate the Program Graphs, it is then processed by a function that translates the list of edges into the syntax for graphviz, and generate a file called graph.dot. This file contains the program graph (consider reading How to interpret program graph results).
The step-wise execution shows how the memory changes throughout the execution of the code and its actions and which nodes each execution takes place.
From the Extended Menu Options, the user can choose to either input variables and arrays themselves or get automated input generated. Afterwards the user chooses how many execution steps they want shown. This will then initialize the Step-Wise Execution and generate a file called StepExecution.txt. This file contains the step-wise execution of the program, consider reading How to interpret the Step-wise Execution.
The outcome:
Is a "Pretty Printed" AST, that shows how the arithmetic, boolean or other commands are being treated by the Parser and Lexer.
Example:
| Input | Outcome | Underlying AST |
|---|---|---|
if true -> x:=2 fi |
if True -> x:=2 fi |
IFFI ( TRUE -> x:= 2) |
if x>=y -> z:=x [] y>x -> z:=y fi |
if x>=y -> z:=x [] y>x -> z:=y fi |
IFFI ( GREATEREQUAL ( x,y ) -> z := x [] GREATER ( y,x ) -> z := y ) |
do true -> skip od |
do True -> skip od |
DOOD ( TRUE -> SKIP) |
dax := ln 1 |
dax := ln(1) |
dax := LN ( 1 ) |
x:=3*(4^2+5) |
x := 3*((4^2)+5) |
x := TIMES( 3, ADD( POW(4, 2), 5)) |
These examples show a clear image of how the AST is formed by the combined work of the Parser and Lexer.
Parse errors are implemented in our GCL-parser, and should yield an error message, if the Lexer recognizes strings that are not defined.
If for some reason an error occurs while running an already defined syntax, then please contact the creators.
The outcome:
When running option 2. Non-Deterministic Program Graph or 3. Deterministic Program Graph from the Main Menu. A file named graph.dot will be generated, where the syntax of the graphviz text language will be inside. The syntax will change each time the program is run, depending on the input of the Guarded Command Language.
If using VS-code and extension has been downloaded, the graph can be previewed directly in the same window. Otherwise this link might help. The syntax of the graph.dot can be dragged and dropped, and hereby shown in graph format.
The outcome:
When running option 1. Step-wise Execution with Automatic Input or 2. Step-wise Execution with User Input from the Extended Menu Options. A file named execution.txt will be generated, where the syntax of step-wise execution is written in the following manner:
Action: ____
Node: ___
Memory->
Boolean memory: ___ = true
Arithmetic memory: <variable> = <value>
Array memory: <array> = [<list>]
Action denotes the action which has been done, could be assignment of a variable or a boolean check.
Node denotes the note where the the program ends up after the action has been done.
Memory denotes the memory with the new variables after the action has been executed.
The step-wise execution of the input Guarded Commands will run either until it is terminates, gets stuck or runs out of amount of steps. The amount of steps shown is user-input, thus the number inputted may not be sufficient enough for the step-wise execution to either terminate or get stuck. The program can then be run again with a larger amount of steps to determine whether or not the program terminates or gets stuck later on.
Depending on whether the program terminates or gets stuck, one of the following messages will be shown.
If the program executes until it runs out of possible steps, the following is printed:
#INSUFFICIENT Program has run out of executing steps
OR if it TERMINATES by achieving the final node, the following message will be shown:
#TERMINATED Program has reached final node.
If the program gets STUCK with the given variables and within the set amount of steps, the following message will be given, providing information on where the program gets stuck, why it gets stuck and with how many steps left:
#STUCK No further edge can be taken. Program is stuck in node __ with __ steps left.
with one of the possible errors (or one of the F# Compiler exceptions):
ERROR: Unknown arithmetic variable __ in expression.
ERROR: Unknown boolean variable __ in expression.
ERROR: Invalid lookup of index __ in array __
According to the annotations provided in the program, the tool we built establishes the covering nodes of the program graph:
1. Initial q▷ and final q◀ node
2. A node for each loop contained in the graph.
Based on this domain of covering nodes, the short path fragments are computed and printed in their corresponding file ShortPathFragments.txt, as in the snippet below, based on an iteration computing the sum:
q▷ x:=0 i:=1 q2
q2 !(i<=n) q◀
q2 i<=n x:=(x+i) q2
Eventually, having predicate assignments for each of these nodes, the tool computes the Proof Obligations of the program verification and prints them in the file ProofObligations.txt:
[(x=0)∧(n>0)] x:=0 i:=1 [(i<n)∧(x>=i)]
[(i<n)∧(x>=i)] !(i<=n) [i>=n]
[(i<n)∧(x>=i)] i<=n x:=(x+i) [(i<n)∧(x>=i)]
Along the proof tree of each fragment some inference rules are applied from the ending predicate P(q◀) (bottom-up). Thus, a predicate B to be implied from the start predicate is obtained and the verification condition P(q▷) => B is formed. All of them are printed in the file VerificationConditions.txt:
(x=0)∧(n>0) => (1<n)∧(0>=1)
(i<n)∧(x>=i) => ((i<n)∧((x+i)>=i))∧(i<=n)
(i<n)∧(x>=i) => (i>=n)∧(¬(i<=n))
Sign Analysis:
Sign Analysis is an interpretation of a given program, where initial signs defining the values of the variables and array contents are evaluated dynamically based on programs nodes/edges.
The sign analysis is not a concrete analyzing tool, since it utilizes abstract memories and operators such as:
| ⨣ | - | 0 | + |
|---|---|---|---|
| - | {−} | {−} | {−, 0, +} |
| 0 | {−} | {0} | {+} |
| + | {−, 0, +} | {+} | {+} |
When running the Program Sign Analysis in the menu, the user will be asked to provide some initial sign information.
The signs available are the set {-,0,+}. The information for each field should be delimited by comma ','.To enforce the sign for a variable use a=+ and for an array use A={+,-}. If a variable or array is missing in declaration of signs, it would be automatically assigned to +.
The outcome:
The output of the tool will be sent to the file SignAnalysis.txt.
Here the user will be able to see the solutions for the final node(q◀) and initial node(q▷) (pay attention to the order in the file), and the other nodes (numbered) with their respective sign analysis assignment, in the following format:
Node --> q5
Sign Analysis ->
Variables: i <=> + | j <=> 0 | n <=> + | t <=> + | x <=> - |
Arrays: A <=> + |
Sign Analysis ->
Variables: i <=> - | j <=> + | n <=> + | t <=> + | x <=> + |
Arrays: A <=> + - 0 |
Sign Analysis ->
Variables: i <=> + | j <=> - | n <=> + | t <=> 0 | x <=> + |
Arrays: A <=> + |
Security Analysis:
Security Analysis is a form of verification of a program's information flows. Based on a security lattice and a classification of variables, selected by the user, the tool can compute if any violations of information flows are present in the program or if the program is secure in that aspect. This analyzing tool can only be applied on deterministic program graphs.
The security lattice can be defined by specifying information flows from one security level to another public -> private, trusted -> dubious, delimited by commas , . The security lattice is considered valid, if it is a partially ordered set and can be illustrated in a Hasse diagram.
If no security lattice is provided or the one provided is not a poset (partially ordered set), the user can choose from 4 predefined security lattices in the respective menu:
- Confidentiality: public ⊑ private
- Integrity: trusted ⊑ dubious
- Classical: low ⊑ high
- Isolation: clean ⊑ Facebook, clean ⊑ Google, clean ⊑ Microsoft
The security classification can be defined by providing a security level for each variable appearing in the program x = public, y = private, delimited by commas , . Any missing variable classifications will be assigned automatically.
The user has to provide all the information either from the console or from a specified file.
The Outcome:
The output of the analyzing tool is redirected to the file SecurityAnalysis.txt.
In the first rows, the security lattice and security classification chosen are presented for context:
Security lattice configuration:
classified ⊑ top_secret; private ⊑ classified; public ⊑ private;
Security classification memory:
A ∈ classified; i ∈ public; j ∈ private; n ∈ top_secret; t ∈ classified;
Following, the user will be able to analyze the set of flows actually happening in the program and the set of flows allowed to happen in the program according to the lattice rules:
Set of actual information flows in the program:
A->A; A->j; A->t; i->A; i->i; i->j; i->t; j->A; j->j; j->t; n->A; n->i; n->j; n->t; t->A;
Set of allowed information flows in the program:
A->A; A->t; i->i; i->j; j->A; j->j; j->t; t->A;
Finally, based on the above sets, the tools finds all the violations of information flow in the program and outputs them. If the set of violations is empty, the program is considered SECURE and INSECURE, otherwise:
Program is not secure!
Violations of information flow: A->j; i->A; i->t; n->A; n->i; n->j; n->t;
Model Checking:
Model Checking is an analysis that checks whether the programs gets stuck or run smoothly depending on initial memory input from the user. The analysis is only available when considering Non-Deterministic graphs.
The Outcome:
After choosing the GCL-program and the initial input, the Model Checking analysis will take place.
The result will be printed into the file ModelChecking.txt.
The result can be displayed in two ways:
- Successful: if the program runs correctly the output will only be of the final node
- Unsuccessful: if the program gets stuck, the current state and an error message are going to be printed:
Example of unsuccessful configuration:
STUCK Node: q3 <=> Memory:
Boolean memory:
Arithmetic memory: i = 3.000000 j = 3.000000 n = 4.000000 t = 1.000000
Array memory: A = [1.0; 2.0; 3.0]
ERROR: Invalid lookup of index 3 in array A
A successful configuration will generate the output line:
Model Checker for given inputs is successful!
This was the end of Computer Science Modelling, we want to give a big thanks to the TA's and our teachers Alberto and Christoph.
Group name: CheckMate
Project completed within DTU course 02141 - Computer Science Modelling