Design and Development of Secure Systems Lecture Slides PDF

SOFT40171 – Design and Development of Secure Systems Week 2 – Formal Specification and Modelling Dr Alexandros Konios 18/02/2025 Agenda  Recall Formal Methods and their importance  What formal specification and modelling are  Their use in system...

SOFT40171 – Design and Development of Secure Systems Week 2 – Formal Specification and Modelling Dr Alexandros Konios 18/02/2025 Agenda  Recall Formal Methods and their importance  What formal specification and modelling are  Their use in system/software development life cycle  Introduction to Automata (or Finite State Machines) Week 2 – Formal Specification and Modelling Learning Objectives Upon completion of this lecture, you should be able to:  Recall Formal Methods aspects and their use for the development of secure systems  Explain what a formal specification is and how it is applied to system development  Two different formal specification approaches  Describe automata and their use in modelling a system’s behaviour Week 2 – Formal Specification and Modelling Formal Methods 18/02/2025 Formal Methods (FMs) What are Formal Methods?  Formal Methods are mathematical-based techniques and tools used to express an intricate system as a mathematical entity.  Can be used to specify, model and verify the structure and behaviour of the examined system. But why we should use Formal methods?  They can be used in any phase/stage of the system development life cycle (SDLC)  Detecting system errors, malfunctioning or inconsistencies in the early development stages. Week 2 – Formal Specification and Modelling Formal Methods in Development Life Cycle Formal Methods are used to describe different aspects of a system and be be applied to different stages of SDLC:  Formal Specification  Associated with Informal Specification.  Used to mathematically express system’s requirements and functioning.  Formal Modelling  Applied to design, development and maintenance stages of the SDLC.  Used to represent the structure and behaviour.  Formal Verification  Applied to analyse the correctness of the developed model w.r.t the system specification.  Complementary to Testing. Week 2 – Formal Specification and Modelling Formal Specification 18/02/2025 Formal Specification Formal Specification is a system specification that is expressed in a mathematical language.  That language has a formalism with well-defined syntax and semantics. A Formal Specification explicitly defines the system functioning and requirements  An excellent way of detecting system specification defects or errors and presenting system specification in an unambiguous way. Week 2 – Formal Specification and Modelling Formal Specification (cont.)  System Specification and System Design overlap  System requirements specification and the formal specification are interrelated.  Early stages of the specification process are determined/defined by the client, while the final stages of that process, which are related to the construction of a complete, consistent and precise formal specification, are defined by the developer/specialist. Figure adapted from Software Engineering (9th Edition) book Week 2 – Formal Specification and Modelling Types of Formal Specification Formal Specification can be distinguished into two fundamental categories of specification techniques:  algebraic techniques  Described as system operations and their relationships  model-based techniques  Described as a model where the system operations are expressed w.r.t the potential state changes Several different formal languages have been proposed and used in each of these two specification categories capturing either the sequential or concurrent behaviour of the examined systems Week 2 – Formal Specification and Modelling Sequential and Concurrent Formal Languages Figure adapted from Software Engineering (9th Edition) book Week 2 – Formal Specification and Modelling Example of Algebraic Specification Figures adapted from Software Engineering (9th Edition) book Week 2 – Formal Specification and Modelling Example of Model-Based Specification Figures adapted from Software Engineering (9th Edition) book Week 2 – Formal Specification and Modelling Benefits and Limitations of Formal Specification Benefits:  Formal specification provides insights into and understanding of the system requirements and design.  Formal specifications may be used as a guide to create test cases for any particular component of the system.  Formal specifications often support  automated processing  Animation/simulation of a specification providing a prototype system Limitations:  Designers and developers are not trained in formal specification techniques.  There is widespread ignorance of current specification techniques and their uses.  Research focuses more on the development of notations and less on the tool support. Week 2 – Formal Specification and Modelling Formal Modelling 18/02/2025 Formal Modelling Formal modelling is the process of specifying the behaviour and structure of a system using a mathematical model.  Sequential or concurrent behaviour and structure of core system components Formal modelling can have different abstraction levels with respect to the representation of the system behaviour.  Depends on system requirements, components and functions are considered in model Week 2 – Formal Specification and Modelling Formal Modelling Languages Formal modelling languages can be distinguished into two main categories with respect to the expression of their models.  Textual languages  Graphical languages Examples of such languages are:  Vienna Development Method (VDM) and Process Algebra  Automata, Petri Nets and Unified Modeling Language (UML) Week 2 – Formal Specification and Modelling Automata or Finite State Machines 18/02/2025 Finite State Machines Finite State Machines (FSMs) can be used in formal specification, verification and testing of systems. FSMs provide an abstract description of the system states.  For instance, one can specify what actions the system can perform in response to an ‘external’ action. There exist different types of FSMs that are used in different stages of the design process. Week 2 – Formal Specification and Modelling Communicating Finite State Machines A Communicating Finite State Machines (CFSMs) can:  Receive messages (signals)  Send messages (signals)  Change their internal state Two or more CFSMs can be combined together resulting in the representation of complex, interactive and concurrent behaviours that can be analysed. Week 2 – Formal Specification and Modelling Formal Definition of Communicating Finite State Machines A Communicating Finite State Machines (CFSMs) is expressed as a tuple: F = (Q, q0, A, T) Where:  Q is a finite non-empty set of states  q0 ∊ Q is the initial state  A is a finite set of communication actions (i.e. actions of the form a! and a?) and is called the alphabet of F.  T : (Q ,(A∪{𝜏})) → Q is the transition relation Week 2 – Formal Specification and Modelling An Example of CFSMs A simple sender-receiver scheme: where a, b and c are channel names Sender receives a signal (message) on channel a and transmits it to Receiver using channel b. Receiver accepts the signal and forwards it using channel c Sender and Receiver behave as one-place buffers (channels with capacity one) Week 2 – Formal Specification and Modelling An Example of CFSMs (cont.) The CFSMs model that represents the behaviour of that system is as follows: Where:  q0 and r0 are the initial states of the CFSMs  a? and a! represent the receiving and sending process over channel a Note: a? and a! are matching messages (signals) Week 2 – Formal Specification and Modelling Observations on Example (1/4) The concurrent composition of the two CFSMs is denoted as: System = Sender || Receiver Possible traces of the CFSMs:  Sender: ⟨⟩ ⟨a?⟩ ⟨a?, b!⟩ ⟨a?, b!, a?⟩ …  Receiver: ⟨⟩ ⟨b?⟩ ⟨b?, c!⟩ ⟨b?, c!, b?⟩ … Week 2 – Formal Specification and Modelling Observations on Example (2/4) Traces generated by System: First attempt: ⟨⟩ ⟨a?⟩ ⟨ a?, b!&b?⟩ ⟨a?, b!&b?, c! ⟩ … Notes:  b!&b? is an internal action which is invisible to the external environment  All internal actions will be denoted by 𝜏 Second attempt: ⟨⟩ ⟨a?⟩ ⟨ a?, 𝜏⟩ ⟨a?, 𝜏, c! ⟩ … After deleting the invisible 𝜏 actions: ⟨⟩ ⟨a?⟩ ⟨a?, c! ⟩ … Week 2 – Formal Specification and Modelling Observations on Example (3/4) States generated by System: Four global states: (q0, r0), ( q0, r1 ), (q1, r0 ), (q1, r1) The global initial state is: (q0, r0) After executing a? at the initial state (q0, r0), the system moves to state (q1, r0). After executing 𝜏 (i.e. b!&b?) at the state (q1, r0), it moves to state (q0, r1). Week 2 – Formal Specification and Modelling Observations on Example (4/4) The concurrent composition of the two CFSMs can be represented by the following CFSM: Where:  a?, c!, etc. are external actions  𝜏 is an internal (invisible or hidden) action Depending on the verification technique used, the system could be treated either as a single CFSM or as a pair of CFSMs. Week 2 – Formal Specification and Modelling Summary The most important points of this session are summarised below:  Formal methods can be used to explicitly define the sequential or concurrent behaviour of systems.  Formal Specification is useful for early detection of system flaws.  Formal modelling provides a range of different modelling languages.  FSMs can be used to efficiently model the behaviour of system expressing the state changes that occur during its operation. Week 2 – Formal Specification and Modelling Any Questions?