CSD 2600 – Coursework 2: Journal Paper on Concurrency and Dropbox It is strongly advised to follow the outline of the Seminars sheets (Seminar 4 and 5) and Lab sheets (Lab 4 and 5). Scenario for the assignment: Concurrency problems with cloud services; service example is Dropbox; a solution is mutual exclusion (Mutex). Simple example scenario: Two users have access to a shared Dropbox folder. Both want to read and write the same file. This may create a concurrency issue. A standard solution is to use a semaphore or a monitor. Assignment Requirements: The journal paper must describe the background of the project, i.e. Concurrency and Dropbox. The Concurrency problem must be illustrated using Finite State Machines (FSM) or Finite State Processes (FSP), and Erlang. The solution (Mutex) must also be illustrated in FSM/FSP and implemented in Erlang. • The background: Dropbox and Erlang • The concurrency problem using some high level description like FSM or FSP. How does this manifest itself in your Erlang implementation? • What is your solution idea/algorithm? (Mutex probably) • Solution in Erlang including some analysis (tests, problems encountered). Formal Journal Requirements: • The report should demonstrate qualities in terms of writing skills, format, and contents. • Maximum 5 pages • NO plagiarism • Your own words with the exception of quotations from other sources that should be highlighted in quotation marks "…" and referenced • The Journal must be written in the provided IEEE format (can be found in the Internet, latex or word. A word template is on Moodle.) • The Erlang source code must be submitted together with the paper as a tared or zipped collection of ASCII files and will be marked for functional correctness and completeness (Solution/Evaluation).Recommended General Journal Paper Structure • Abstract • Summary of your work – very important !! (it is the most read) • Introduction • Places the work in the appropriate context, gently introduces the subject, introduces related approaches and concludes with a roadmap • Background • basic concepts and terminology to understand your work • Possible approaches • Various solutions • Discussion • Critically evaluate all solutions – pros and cons • Future works / improvements (if any) • Conclusions • Summaries and underlines major concepts • References • Look in google scholar • IEEE and ACM digital libraries • NOT JUST WIKIPEDIA Marking Scheme:IEEE Paper Format: Example Investigating Airplane Safety and Security against Insider Threats Using Logical Modeling Florian Kammuller ¨ Middlesex University London [email protected] Manfred Kerber University of Birmingham [email protected] Abstract—In this paper we consider the limits of formal modeling of infrastructures and the application of social explanation for the analysis of insider threats in security and safety critical areas. As an area of study for the analysis we take examples from aviation, firstly since incidents are typically well-documented and secondly since it is an important area per se. In March 2015, a Germanwings flight has crashed in the French Alps in what is quite firmly believed to have been intentionally caused by the copilot who has locked the pilot out of the cockpit and programmed the autopilot on constant descent. We investigate the security controls and policies in airplanes against insider threats using logical modeling in Isabelle. I. INTRODUCTION AND OVERVIEW In this paper, we take a critical look at logical methods to model and analyse safety and security critical systems. In particular, we address recent advances in applying formal verification techniques, e.g. [1], in the context of severe incidents like the tragic crash of a Germanwings flight: "On March 24, 2015 Germanwings Flight 9525, a scheduled flight from Barcelona to Dusseldorf was hijacked by the co-pilot. 30 ¨ minutes after takeoff Andreas Lubitz locked himself in [the] cockpit when [the] captain went out for a rest. Then the copilot started to descend. [The] captain ... tried to communicate with Lubitz, but he didn't reply. After 8 minutes of falling the airplane crashed in the Alps near the French village PradsHaute-Blone. There were 144 passengers and 6 crew members on board. None of them survived the crash." [2] In this paper, we first summarize the development of airplane security (Section II) before we model and analyse the specific settings in passenger transport airplanes using the Isabelle Insider framework (Section III) leading to a discussion and conclusions (Section IV). It should be noted that with insider attacks there are two fundamentally different approaches. The first is based on probabilistic reasoning and cost analysis. For instance, if in a company there is a leakage in low-cost pens, since employees take them home then the company must consider whether imposing a strict control regime involving CCTV cameras is cost effective in eliminating the problem. The company may conclude that cheaper measures minimize the overall cost of lost pens and measures to lose only few. The second approach is based on Boolean reasoning in which it is investigated whether certain attacks are possible or not. That is, a model of a real world situation is built and then it is checked or proved that a particular situation can occur or not, for instance, by checking whether a particular state is reachable from an initial state or not. Such an approach would be applied, for instance, if a particular situation is unacceptable and has to be avoided at all cost. As a consequence, for airplane safety this will be the method of choice and is the approach taken in the following. Of course, this does not mean that the approach gives 100% guarantees. The main problem is that any model of a real world situation is necessarily incomplete since it abstracts from (hopefully only irrelevant) details. However, it is difficult to establish that nothing essential has been overlooked. A. Related Work We consider here some main threads of work by others while discussing the relationship of the contribution of this paper to our own previous work in Section IV. The Insider threat patterns provided by CERT [3] use the System Dynamics models, which can express dependencies between variables. The System Dynamics approach is also successfully being applied in other approaches to Insider threats, for example, in the modeling of unintentional insider threats [4]. Axelrad et al. [5] have used Bayesian networks for modelling Insider threats in particular the human disposition. In comparison, the model we rely on for modeling the human disposition in the Isabelle Insider framework is a simplified classification following the taxonomy provided by [6]. On the other side, compared to all these approaches, our work provides an additional model of infrastructures and policies allowing reasoning at the individual and organisational level. In the domain of rigorous analysis of airplane systems, work often follows for practical and economic reasons a philosophy of using a mix of formal and systematic informal methods. An example from airplane maintenance procedures [7] uses a security evaluation methodology following the Common Criteria and a formal model and verification with the model checker AVISPA. In comparison, we use a more expressive logical model in the Isabelle Insider framework than their AVISPA specification. Also, we believe that our work is the first to consider Insider threats within airplane safety and security at least in a formal way. On the formal side within the Insider threat community in general, the work by Bishop et al [8] is relevant to the Isabelle Insider framework since it also uses a formal model to analyse Insider threats. Bishop and colleagues use the