Course

# An Introduction to Proof Equivalence Teachers: Matteo Acclavio and Paolo Pistone

Classes are evey morning from 11h to 13h

## Course schedule

### Day 1, 7 August: Overview and Motivations

• What is a proof?
• Two approaches to the problem of Proof Identity
• What is a proof system?
• Natural Deduction, Sequent Calculus and rule permutations.
In this class we discuss the notion of proof and how they can be formalized. After underlying the importance of defining a notion of proof equivalence, we provide the two main approaches to this problem we will explore during the course. We recall the definition of proof system by Cook-Reckhow and the sequent calculi and natural deduction systems for both classical and intuitionistic logic. We then analyze the standard rules permutations we can perform on sequent calculus derivations.

Slides and Notes

### Day 2, 8 August: The Paradise of Syllogism and the Forbidden Fruit

• How much information is needed?
• Multiplicative Linear Logic, Proof nets, and units
• Are structural rules canonical?
• Canonicity of structural rules
We show the Multiplicative Linear Logic and how we can represent proofs using proof nets. We show their canonicity w.r.t. sequent calculus derivations. We show then show that as soon as units or structural behaviors are included in a system, then canonicity may become impossible to achieve.

### Day 3, 9 August: Normalization LJ and Denotationional Semantics

• Is natural deduction canonical?
• Natural deduction, normalization and canonicity
• What is a Denotational Semantics?
• Game semantics for Intiotionistic Propositional Logic

#### Bibliografy:

We show the canonicity of disjuntion-free fragment natural deduction with respect normalization and generality. Moreover, in presence of disjunction we can make obtain canonicity with respect to normalization but not with respect to generality. We then define the notion of denotational semantics. We show how a denotational semantics can be easily defined in term of quotient, we show how Game Semantics provides a concrete model for such a semantics.

### Day 4, 10 August: Overview

• Why normalization is not suitable for proof equivalence in classical logic?
• Reducing non-determinism via Focusing
• How much non-determinism can we get rid of?
• Combinatorial Proofs for Classical Logic

#### Bibliografy:

We show the impossibility of having a non-trivial denotational semantics for classical logic by presenting Lafont critical pairs and Joyal's argument. We then present some refinement of sequent calculi allowing to reintroduce canonicity by reducing the non-determinism in proof search. We conclude by introducing the syntax of combinatorial proofs for classical logic, a graphical syntax suitable to provide a canonical representation of proofs. We discuss which rule permutations are captured by this syntax and we discuss the extension of this syntax to other logic.

### Day 5, 11 August: Overview

• Proof equivalence in first and second order logic
• Why computer scientist should care about proof equivalence?
• Applications to real world problems
We introduce first and second order quantifiers, and the calculi for first and second order classical and intuitionistic logic. We show the additional challenges in proof equivalence for these logics, and the partial results in the literature. We conclude the course by illustrating applications of proof equivalence to verification, interoperability of theorem provers and suggests the current trends in proof theoretical approaches to programming language theory.

# Security 2

Courses classes are Thursday form 9h45 to 11h15 online (the link is available on the moodle)

## Evaluation:

• Attack trees presentations (30%)
• Evaluation on information flows (20%)
• Homeworks on Proverif (50%)

## Course schedule

### Week 1, 18 February: Overview

• What does security mean?
• Secure systems need good design:
• Evaluate potential risks
• Risk assessment and cost models
• Risk prevention/incentives

What Is Security Engineering

### Week 2, 25 February: Attack Trees

• Risk management

• security risk = possible damage
• Identify risks
• Reduce risks
• Keep other risks under control during this operation
• Repete...
• Glossary:
• Asset = something of Evaluate
• Vulnerability = a weakeness of the system which can be exploited to harm the asset
• Threat = exploitation of a vulnerability by a threat agent
• Risk = quantification of a threat
• Control = measure to reduce a risk
• How to do risk analysis?
• identify context
• identify assets
• assess risks
• treat risks
• Classify threats (impact vs likelihood)
• Possible controls:
• acceptance
• avoidance
• transfer
• possible treatments: accept risks, reduce impact, reduce likelihood
• Controls have costs or may not be 100% effective
• Attack Trees

• free lunch tree example
• threat Trees
• fault Trees
• Tree nodes are AND, OR, SAND, KofN ...
• Attack Trees semantics

• Why semantics? (distinguis equivalent trees)
• propositional/set semantics
• multiset semantics
• Computing Attributes

• possible attribute domains: cost, probability, possibility, time, ...
• possibility = boolean circuits
• cost = OR -> minimum of children values / AND -> sum of children values
• probability = OR -> probability of union / AND -> probability of intersection

### Week 3, 4 March: free meal case study

• Attack trees Evaluation:
• case analysis of the free-meal attack tree
• loss
• time
• probability
• focus on nodes refinements types

### Week 4, 11 March: Students presentations

During this class students will give short presentations of some attack trees they produce. Each presentation must include

• Presentation of the problem:

• identify the attack
• identify the context
• cite if any source has been used to construct the tree (students are authorised to use public available material by citing it)
• provide the attack tree of the chosen attack by justifying some design choices, e.g.:
• why a conjunctive/disjunctive refinement
• why only considering some refinements/node children and not others
• ...
• Minimal Tree Size:
• minimal height = 2 , that is, there must be a path of lenght 2 from the root to a leaf
• minimal width = 5 , that is, the tree must have at least 5 leaves
• Evaluations using the tree:

• chose (at least) two attributes
• explicit attribute domains. E.g., probabilities may be expressed in percentage, or using real numbers in the interval [0,1], or using some meta-attribute like impossible/unlikely/likely/surely
• explicit how the attributes have been assigned to the leaves of the tree as public available statistics, experts evaluations... or as arbitrary decision of the student
• chose who estimates the attributes (attacker or defender)
• fix an evaluation method. By means of example, the cost value of a disjunctive node may be the minimum of the value of its children, while for the loss value of a disjunctive node we may be the maximum of the value of its children.

### Week 5, 15 March (Matteo): Control Access Models

• Access control policies: determine who has access to what (and when) in a system
• Discretionary Access Control (DAC): users decide
• each resource has an owner
• Troyan horse information leak: Alice owns a file Info which cannot be accessed by Bob. A Troyan-horse (executed as Alice) may read Info and copy on a file Stole owned by Bob, allowing Bob to read the content of Info.
• Mandatory Access Control (MAC): system decides
• each user and security has a security Labels
• if labels match some conditions, then access is guaranteed
• resource access must not change during import/export of datas
• Role Based Access Control (RBAC): roles decides
• each user has a role
• roles determine access rights
• Principles:
• least privilege: each user should have the minimal access privileges to accomplish its tasks
• separating duties: avoid to have users with too much power
• policies combination: combine policies for finer access control
• Terminology:
• Users: active in the system.
• Objects: passive in the system.
• Access rights: read, write, execute, delede, create, switch, move, ...
• System description: (S, O, A, M: S x O -> P(A)) where
• S = set of subjects
• O = set of Objects
• A = set of access rights
• M: S x O -> P(A) = matrix associating to every subject and object a set of access rights in A
• in MAC there is also:
• (L,>) = partially ordered set of labels
• l: S U O -> L = labeling function associating a label to each object and subject

[The model preserves confidentiality but not integrity of data!]

• Simple security rule [or ss-rule] (no read up): a subject s can read an object o only if l(s)=l(o) or l(s)>l(o)
• *-Property (no write down): a subject s can write an object o only if l(s)=l(o) or l(s)<l(o)
• Discretionary security property [or ds-property]: users can grant access to objects according with ss-rule and *-property

#### State of a system

• (C, M, l) where
• C = configuration / current access status: it is given by a set of triple of the form (s,o,a) in S x O x A
• M and l are respectively the access matrix and the label function (which may be updated)
• Possible evolutions (operational semantic rules):
• add (s,o,a) to C when s get the access right a to o
• remove (s,o,a) from C when s release the access right a to o
• change l(s) when the security label of s is changed
• change l(o) when the security label of o is changed
• add a to M(s,o) to give s the access right a on o
• remove a from M(s,o) to rescind s the access right a on o
• a subset C of S x O x A may evolve to C' if C' may be obtained by applying operational semantic rules to C

### Week 6, 22 March (Matteo): Chinese Wall

• In the Bell-LaPadula model if a configuration C satisfies the ss-rule, *-property and ds-property, then any confuguration C' which may be obtained by applying operational semantic rules to C does.
• S:={Alice, Bob}
• O:={Info, Stole}
• M:=
Alice Bob
• (L,<):= ({top,bot} , top<bot)
• l: S U O -> L:=
l(Alice)=l(Info)=top and l(Bob)=l(Stole)=bot
• the initial configuration is the empty one, the final configuration should be

#### Chinese Wall or Brewer-Nash (DAC + Mandatory access)

• objects have owners (companies databases)
• each company belongs to a conflic of interest class
• you can think that every object has a label (owner, owner's conflict of interest class)
• SS-rule: a subject s can read an object o belonging to a company x only if
• s had no access to any object in a different company x' in the same conflict of interest class
• *-Property: a subject s can write an object o belonging to a company x only if

### Spring break (week of the 5th of April) # CS2040 - Spring course 2020

Courses classes are on Monday, Wednesday and Thursday form 1h45 to 3h05 in room PL-5 (2bis, Passage Landrieu).

## Textbook

INTRODUCTION TO. JAVA. PROGRAMMING (10th Edition) by Daniel Jiang

## Online resurces

### Java

• W3shool: usefull website with tutorial and explainations;
• geekforgeek: another usefull website;
• stackoverflow: if you have a really weird code problem, it probably has already be solved here;

### Base 2 integer conversion

From base 10 to base 2 and

### Linear Feedback Shift Register ### The "De Brujin" magic trick

!! their card encoding may not corresponds to the one proposed in this exercise!!
• the math behind;
• the trick in action 1
• the trick in action 2

### Exceptions

Exceptions have to be excaptional!
Some in-depth articles on When and How to use or avoid exceptions:

### JavaFX

If you have problems with JavaFX and eclipse on your laptop (like me), you can download IntelliJ (community version) and follow these instructions;

## Program of the course

Date Content Assignments
Week 1:
Gen 13
Introduction
• Introduction to the course and the course Web site
• Compilers and IDE
• Introduction Slides
!! Class only on Monday 13 !!
• Ex1 Part1
• try Part 2
Week 2:
Gen 20 at 13h45
Gen 23 at 13h45 and at 15h20
Types
• Data type
• Program type
• Type casting
• An elementary encryption method: Caesar cipher
• Encrypting via LFSR
No class on Wednesday 22, double class on Thursday 23
• Write a Caesar cipher encripting program
• Revise course CS1040 topics: Chapters 1-8 of the book (see also myProgrammingLab exercises)
Week 3:
Gen 27 at 13h45
Gen 29 at 13h45
Gen 30 at 13h45 and at 15h20
Objects and Classes
• What is a class?
• Unified Modeling Language
• this
• What is an object?
• Differences between objects and classes
• Why to use OOP?
• Programming paradigms (procedural vs OOP)
• here our zoo classes
! Double class on Thursday 30 !
• Book chapter 9
• Give feedback to at least 2 peergrade submissions
• myProgrammingLab exercises on book chapter 9 (at least the two projects at the end of the chapter)
Week 4
Feb 3 at 13:55
Feb 5 at 13:45
Feb 6 at 13:45
OOP thinking & Inheritance & Abstract Classes
• Why to use OOP?
• Data access
• Association
• Subclasses
• Inheritance
• super
• Polymorphism
• here our new zoo
• ArrayList
• Excercise: social network (the code we wrote in class)
• Book chapter 10 & 11 & 13
• myProgrammingLab exercises on chapter 10
• myProgrammingLab projects of chapter 11
Week 5
Feb 10 at 13:55
Feb 12 at 13:45
Feb 13 at 13:45
Excercises
• Some exercises on the point of the plane (solution w.i.p.)
• Solution of assignement 2
• Assignement 2
• Revise Book chapters 9-11 & 13
• myProgrammingLab exercises on chapter 10
• myProgrammingLab projects of chapter 11
17.2 - 28.2 Spring Break
Revise Chapters form 1 to 11 and 13, focussing on 9-11 and 13.
Pay attention to the following key concept summarized in the Chapters Summary (at the end of each Chapter):
• Chapter 2: 9-12, 17;
• Chapter 3: 1, 4-6;
• Chapter 4: 2, 8-11;
• Chapter 6: all;
• Chapter 7: 1-9;
• Chapter 9: all;
• Chapter 10: 1, 2, 3;
• Chapter 11: all;
• Chapter 13: 1-6, 9, 10;
Keep in practice with coding
Week 6
2.3
Midterm Exam
• Theory Test
• Programming Test
! No class on Wednesday 4 !
Book chapters 1-11 & 13
Week 7
9.3
Exception handling and Text I/O
• exceptions and exception handling
• Try-Catch
• File class
• create/rename/delede files
• write data to a file
• read data from a file
• Excercises
• ! No class on Monday 9 !
• Book chapter 12.1-12.11
• myProgrammingLab exercises on book chapter 12
Week 8
16.3
Excercises on File
• Book chapter 12.10-12.11
• myProgrammingLab exercises on book chapter 12
Week 9
23.3
JavaFX

Scene Builder and Gluon are visual layout tools design GUI.
First steps using scene builder. More details on using scene builder.
With and without scene builder.

• Book chapter 14, suggested order: from 14.1 to 14.4 -> 14.10 -> from 14.5 to the end
• First step tutorial: How to create a new windows
• A more detailed tutorial on JavaFX
• Send me your final project proposal [What kind of application you want to develop?]
Week 10
30.3
Event Driven Programming and some more JavaFX
• Event source
• MouseEvent
• KeyEvent
• Animations: Animation, PathTransition, FadeTransition, and Timeline
• Label and Buttons
• Book chapter 15 untill 16.4
• Try to make run the boinching ball example a the end of chapter 15
Week 11
6.4
JavaFX and I/O
• TextField
• ComboBox and ListView
• To view and play video and audio
• Book chapter 15
• Start to implement the GUI of your final project
• Try to make this Connection Four look like this.
Week 12
13.4
Recursion
• Recursion in programming
• Factorial
• Fibonacci numbers
• Fractals
• book chapters 17 and 18
• Send me at least a static (does not change by user interaction) but working (that is compiling and showing all the components) graphical interface for your final project before Thursday the 16th.
Week 13
20.4
Recursion and Complexity
• Last project revision
• Recursion vs Iteration
• Complexity: O(n) notation
• What is the complexity of an algorythm?
• Complexity of sorting algorithms
• Complexity: 1000000\$ Problems
• Chapter 22-23
• Send me your first version of the final project before Thursday the 23th
Week 14
27.4
class only on Monday: course recap and project revision.