Formal Methods and Software Engineering: 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1–3, 2021, Proceedings

Preface
Organization
Contents
Safety and Security
Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-agent Systems
1 Introduction
2 Attack-Defence Trees
2.1 The Basic ADTree Model
2.2 Attributes and Agents for ADTrees
2.3 Example: Treasure Hunters
3 AMAS
4 Extending the AMAS Model
5 EAMAS Transformation of ADTrees
5.1 Transformation Patterns
5.2 Adding Node Attributes
6 Experiments
6.1 Case Studies
6.2 Experimentation Setup
6.3 Verifying Correctness
6.4 Playing with Agents Coalitions
6.5 Parameter Synthesis
7 Conclusion and Future Work
References
Robustness and Failure Detection in Epistemic Gossip Protocols
1 Introduction
2 Related Work
3 Basic Concepts
3.1 Modeling Agent Failure
3.2 Epistemic Logic
4 Analysis of Robustness and Failure Detection
4.1 Properties on Robustness
4.2 Analysis of Failure Detection
5 Conclusions and Future Work
References
Reasoning with Failures
1 Introduction
2 SIS and FMR
3 Modelling Failures
4 Failure Mode Reasoning
5 Individual Function Blocks
6 FMR in Practice
7 Discussion and Related Works
8 Conclusion
References
Program Verification
Verification of Programs with Pointers in SPARK
1 Introduction
2 Informal Overview of Alias Analysis in SPARK
3 SPARK Language
4 Access Policies, Transformers, and Alias Safety Rules
5 Implementation and Evaluation
6 Related Work
7 Future Work
8 Conclusion
A Semantics for SPARK statements
References
Automated Temporal Verification of Integrated Dependent Effects
1 Introduction
2 Overview
2.1 Integrated Dependent Effects
2.2 Forward Verification
2.3 The T.r.s
3 Language and Specifications
3.1 Target Language
3.2 The Specification Language
3.3 Semantic Model of Effects
4 Automated Verification
5 Effects Inclusion Checker (the T.r.s)
6 Implementation and Evaluation
6.1 Case Studies
6.2 Experimental Results
7 Related Work
7.1 Verification and Expressive Effects
7.2 Efficient Algorithms for Language Inclusion Checking
8 Conclusion
References
A Reversible Operational Semantics for Imperative Programming Languages
1 Introduction
2 Preliminaries: SIMP
3 RIMP: A Reversible Imperative Language
4 A Program Inverter for RIMP
5 Reversing the Computations in RIMP
6 Related Work
7 Conclusions and Future Work
References
Parallel Chopped Symbolic Execution
1 Introduction
2 Background
2.1 Parallel Symbolic Execution
2.2 Chopping in Symbolic Execution
3 Illustrative Example
3.1 Prefix Generation in Chopper
3.2 Prefix Generation in PChop
4 Approach
4.1 Prefix Generation
4.2 Parallel Execution
5 Evaluation
5.1 Subjects
5.2 Methodology
5.3 Results
6 Related Work
7 Limitations
8 Conclusions
References
Formal Methods and Machine Learning
PAC Learning of Deterministic One-Clock Timed Automata
1 Introduction
2 Preliminaries
2.1 Deterministic One-Clock Timed Automata
2.2 Exact Learning Algorithm for DOTAs
2.3 PAC Learning of DFA
3 PAC Learning of DOTA
3.1 PAC-Style Correctness
3.2 PAC-Style Equivalence Query
3.3 Sampling Mechanism
3.4 Comparator
3.5 Counterexample Minimization
3.6 The Whole Procedure
4 Extending PAC Learning to Normal Teacher
5 Implementation and Experimental Results
5.1 TCP Protocol
5.2 Random Experiments
6 Related Work
7 Conclusion
References
Learning Fault Models of Cyber Physical Systems
1 System Description
2 Overview
2.1 Step 1 - Develop Oracles
2.2 Step 2 - Apply Active Automata Learning
2.3 Illustration
3 Implementation
4 Research Questions and Experiments
4.1 How Effective Is Our Approach in Debugging a Real CPS?
4.2 Does Increasing the Size of the Alphabet Increase the Time Overhead Significantly?
4.3 Can Our Approach Effectively Reduce the Length of Discovered Buggy Traces?
4.4 Can Our Approach Find Bugs Effectively?
5 Related Work
6 Conclusion
References
VARF: Verifying and Analyzing Robustness of Random Forests
1 Introduction
2 Related Work
3 Preliminaries
3.1 Robustness Properties
3.2 Satisfiability Modulo Theories
4 Encoding of Decision Trees and Random Forests
4.1 Decision Tree
4.2 Random Forests Classifier
5 Encoding of Robustness Properties
5.1 Verifying Adversarial Robustness
5.2 Verifying Universal Adversarial Robustness
6 Robust Feature Set and Local Robustness Feature Importance
6.1 Robust Feature Set
6.2 Local Robustness Feature Importance
7 Experiments and Analysis
8 Conclusions and Future Work
References
Formal Languages
Type-Based Declassification for Free
1 Introduction
2 Background: Language and Abstraction Theorem
3 Declassification Policies
4 Type-Based Declassification
4.1 Views and Indistinguishability
4.2 Free Theorem: Typing in the Public View Implies Security
5 Related Work
6 Discussion and Conclusion
References
Four-Valued Monitorability of -Regular Languages
1 Introduction
2 Preliminaries
3 Four-Valued Monitorability
4 Computing Four-Valued Monitorability
5 State-Level Four-Valued Weak Monitorability
6 Implementation and Experimental Results
7 Related Work
8 Conclusion
References
Other Applications of Formal Methods
Formally Verified Trades in Financial Markets
1 Introduction
1.1 An Overview of Trading at an Exchange
1.2 Our Contribution
1.3 Related Work
1.4 Organization of the Paper
2 Modeling Trades at Exchanges
2.1 Bid, Ask and Limit Price
2.2 Matching Demand and Supply
2.3 Individually Rational Trades
2.4 Fairness in Competitive Markets
2.5 Liquidity and Perceived-Fairness in the Markets
3 Optimizing Trades in Financial Markets
3.1 A Maximum Matching Mechanism
3.2 Trading at Equilibrium Price
4 Conclusion and Future Works
References
Formalizing the Transaction Flow Process of Hyperledger Fabric
1 Introduction
2 The Architecture of Hyperledger Fabric
2.1 The Central Concepts
2.2 The Transaction Flow
3 Formalizing the Architectural Entities
3.1 Sets and Elements for the Entities
3.2 Inspection and Update of the Entities
3.3 Illustrative Examples
4 Formalizing the Transaction Flow
4.1 Specification of the Transition Relation
4.2 Conditions for the Transitions
4.3 Illustrative Examples
5 Proving Preservation of Consensus
6 Conclusion
References
Embedding Approximation in Event-B: Safe Hybrid System Design Using Proof and Refinement
1 Introduction
2 Event-B: A Refinement and Proof State Based Method
3 Hybrid Systems Modelling Features
3.1 A Theory of Continuous Mathematics
3.2 A Theory of Approximation
4 Modelling Hybrid Systems Using Event-B
4.1 Generic Model and Its Refinement
4.2 Proof Obligations
4.3 Instantiation of the Generic Model
5 Our Framework
5.1 Limitations: Exact vs Approximate Refinement
5.2 Approximate Refinement
5.3 Formalising Approximate Refinement in Event-B
5.4 Proof Obligations: Revisited for Approximate Refinement
5.5 Exact Refinement as a Particular Case of Approximate Refinement
6 Case Study
6.1 Problem Statement
6.2 System Requirements
6.3 Refinement Strategy
6.4 Event-B Development
7 Conclusion
References
Formal Foundations for Intel SGX Data Center Attestation Primitives
1 Introduction
2 Related Work
2.1 Secure Remote Execution
2.2 Formalizations by Intel
2.3 Discussion
3 Proposed Approach
3.1 Symbolic Model
3.2 Adversary Model
3.3 Security Properties
4 Industrial Case Study: Non-QVE Based DCAP
4.1 Symbolic Model Generation
4.2 Formalization and Verification of Properties
5 Conclusion
References
Short Papers
Towards Modeling and Verification of the CKB Block Synchronization Protocol in Coq
1 Introduction
2 Preliminaries
2.1 The Block Synchronization
2.2 The CKB Block Synchronization Protocol
3 Modeling and Verifying the Protocol in Coq
3.1 Connecting Header Stage
3.2 Downloading Block Stage
3.3 Accepting Block Stage
4 Attack Simulation
5 Conclusion and Future Work
References
Accurate Abstractions for Controller Synthesis with Non-uniform Disturbances
1 Introduction
2 Preliminaries
2.1 Notation
2.2 Systems and Refinement
2.3 Time-Sampled Control Systems
3 Computation of Abstraction
3.1 A Generic Construction
3.2 Growth Bound Computation
3.3 ComputeAbs: Abstraction Algorithm
4 Experimental Results
References
Formalising Privacy-Preserving Constraints in Microservices Architecture
1 Introduction
2 Privacy Issues in Modern Software Design
3 Background: Event-B and ProB
4 Verification of Privacy-Preserving Constrains in MSA Using Event-B
4.1 Approach Description
4.2 Application of the Approach to the EHR Example
5 Related Work and Conclusions
References
Algebraic Approach for Confidence Evaluation of Assurance Cases
1 Introduction
2 Related Work
3 Goal Structuring Notation (GSN)
4 Truthmaker Semantics and Confidence
4.1 Truthmakers
4.2 Frame, Interpretation, and Confidence
5 Relation to Probabilistic Evaluation
6 Multi-legged Argument
7 Concrete Example
8 Conclusion and Future Work
References
Doctoral Symposium Paper
Verification of a TLSF Algorithm in Embedded System
1 Background
2 Verification
Outline placeholder
2.1 Global Nature
2.2 The Function of Allocate
2.3 The Function of Release
3 Conclusion and Future Work
References
Author Index