The use of Internet services and web applications has grown rapidly because of user demand. At the same time, the number of web application vulnerabilities has increased as a result of mistakes in the development where some developers gave the security aspect a lower priority than aspects like application usability. An SQL (structure query language) injection is a common vulnerability in web applications as it allows the hacker or illegal user to have access to the web application's database and therefore damage the data, or change the information held in the database. This thesis proposes a new framework for the detection and prevention of new and common types of SQL injection attacks. The programme of research is divided in several work packages that start from addressing the problem of the web application in general and SQL injection in particular and discuss existing approaches. The other work packages follow a constructive research approach. The framework considers existing and new SQL injection attacks. The framework consists of three checking components; the first component will check the user input for existing attacks, the second component will check for new types of attacks, and the last component will block unexpected responses from the database engine. Additionally, our framework will keep track of an ongoing attack by recording and investigating user behaviour. The framework is based on the Anatempura tool, a runtime verification tool for Interval Temporal Logic properties. Existing attacks and good/bad user behaviours are specified using Interval Temporal Logic, and the detection of new SQL injection attacks is done using the database observer component. Moreover, this thesis discusses a case study where various types of user behaviour are specified in Interval Temporal Logic and show how these can be detected. The implementation of each component has been provided and explained in detail showing the input, the output and the process of each component. Finally, the functionality of each checking component is evaluated using a case study. The user behaviour component is evaluated using sample attacks and normal user inputs. This thesis is summarized at the conclusion chapter, the future work and the limitations will be discussed. This research has made the following contributions: • New framework for detection and prevention of SQL injection attacks. • Runtime detection: use runtime verification technique based on Interval Temporal logic to detect various types of SQL injection attacks. • Database observer: to detect possible new injection attacks by monitoring database transactions. • User's behaviour: investigates related SQL injection attacks using user input, and providing early warning against SQL injection attacks.

Every day, the growing number of viruses causes major damage to computer systems, which many antivirus products have been developed to protect. Regrettably, existing antivirus products do not provide a full solution to the problems associated with viruses. One of the main reasons for this is that these products typically use signature-based detection, so that the rapid growth in the number of viruses means that many signatures have to be added to their signature databases each day. These signatures then have to be stored in the computer system, where they consume increasing memory space. Moreover, the large database will also affect the speed of searching for signatures, and, hence, affect the performance of the system. As the number of viruses continues to grow, ever more space will be needed in the future. There is thus an urgent need for a novel and robust detection technique. One of the most encouraging recent developments in virus research is the use of formulae, which provides alternatives to classic virus detection methods. The proposed research uses temporal logic and behaviour-based detection to detect viruses. Interval Temporal Logic (ITL) will be used to generate virus specifications, properties and formulae based on the analysis of the behaviour of computer viruses, in order to detect them. Tempura, which is the executable subset of ITL, will be used to check whether a good or bad behaviour occurs with the help of ITL description and system traces. The process will also use AnaTempura, an integrated workbench tool for ITL that supports our system specifications. AnaTempura will offer validation and verification of the ITL specifications and provide runtime testing of these specifications.

"Timing diagrams are used in industrial practice as a specification language of circuit components. They have been formalized for efficient use in model checking. This formalization is often more succinct and convenient than the use of temporal logic. We explore the relationship between timing diagrams and temporal logic formulas by showing that closure under disjunction does not hold for timing diagrams. We give an algorithm that returns a disjunction (if any) of two given timing diagrams. We also give algorithms that decide satisfiability of a timing diagram and return exact time separations between events in a timing diagram. An Alloy specification for timing diagrams with one waveform has also been built."

This thesis is about automated reasoning in quantified modal and temporal logics, with an application to formal methods. Quantified modal and temporal logics are extensions of classical first-order logic in which the notion of truth is extended to take into account its necessity or equivalently, in the temporal setting, its persistence through time. Due to their high complexity, these logics are less widely known and studied than their propositional counterparts. Moreover, little so far is known about their mechanisability and usefulness for formal methods. The relevant contributions of this thesis are threefold: firstly, we devise a sound and complete set of sequent calculi for quantified modal logics; secondly, we extend the approach to the quantified temporal logic of linear, discrete time and develop a framework for doing automated reasoning via Proof Planning in it; thirdly, we show a set of experimental results obtained by applying the framework to the problem of Feature Interactions in telecommunication systems. These results indicate that (a) the problem can be concisely and effectively modeled in the aforementioned logic, (b) proof planning actually captures common structures in the related proofs, and (c) the approach is viable also from the point of view of efficiency.

This thesis considers the problem of a robot with complex dynamics navigating a partially discovered environment to satisfy a temporal logic formula consisting of both a co-safety formula component and a safety formula component. We employ a multi-layered synergistic framework for planning motions to satisfy a temporal logic formula, and we combine with it an iterative replanning strategy to locally patch the robot's discretized internal representation of the workspace whenever a new obstacle is discovered. Furthermore, we introduce a notion of ``closeness'' of satisfaction of a linear temporal logic formula, defined by a metric over the states of the corresponding automaton. We employ this measure to maximize partial satisfaction of the co-safety component of the temporal logic formula when obstacles render it unsatisfiable. For the safety component of the specification, we do not allow partial satisfaction. This introduces a general division between ``soft'' and ``hard'' constraints in the temporal logic specification, a concept we illustrate in our discussion of future work. The novel contributions of this thesis include (1) the iterative replanning strategy, (2) the support for safety formulas in the temporal logic specification, (3) the method to locally patch the discretized workspace representation, and (4) support for partial satisfaction of unsatisfiable co-safety formulas. As our experimental results show, these methods allow us to quickly compute motion plans for robots with complex dynamics to satisfy rich temporal logic formulas in partially unknown environments.

Discrete event systems (DESs) are systems which involve quantities that take a discrete set of values, called states, and which evolve according to the occurrence of certain discrete qualitative changes, called events. Examples of DESs include many man-made systems such as computer and communication networks, robotics and manufacturing systems, computer programs, and automated trac systems. Supervisory control and failure diagnosis are two important problems in the study of DESs. This dissertation presents a temporal logic approach to the control and failure diagnosis of DESs. For the control of DESs, full branching time temporal logic-CTL* is used to express control specifications. Control problem of DES in the temporal logic setting is formulated; and the controllability of DES is defined. By encoding the system with a CTL formula, the control problem of CTL* is reduced to the decision problem of CTL*. It is further shown that the control problem of CTL* (resp., CTL{computation tree logic) is complete for deterministic double (resp., single) exponential time. A sound and complete supervisor synthesis algorithm for the control of CTL* is provided. Special cases of the control of computation tree logic (CTL) and linear-time temporal logic (LTL) are also studied; and for which algorithms of better complexity are provided. For the failure diagnosis of DESs, LTL is used to express fault specifications. Failure diagnosis problem of DES in the temporal logic setting is formulated; and the diagnosability of DES is defined. The problem of testing the diagnosability is reduced to that of model checking. An algorithm for the test of diagnosability and the synthesis of a diagnoser is obtained. The algorithm has a polynomial complexity in the number of system states and the number of fault specifications. For the diagnosis of repeated failures in DESs, different notions of repeated failure diagnosability, K-diagnosability, [1,K]-diagnosability, and [1,1]-diagnosability, are introduced. Polynomial algorithms for checking these various notions of repeated failure diagnosability are given, and a procedure of polynomial complexity for the on-line diagnosis of repeated failures is also presented.

Extending Descriptions Logics (DLs) with a temporal dimension to aid in the ability to model meaningful temporal information is an active and popular research area that has gathered a lot of attention over recent years. DLs underpin the Web Ontology Language (OWL) which offers a way to describe ontologies for the semantic web. Representing temporal information in ontologies plays an important role, specifically for those ontologies where time information is inherently embedded in the information they describe. This is very common for ontologies in the bio-health domain, for example ontologies that describe the development of anatomies of biological entities, stage based development, evolution of diseases and so on. As expressive as DLs are, given that they are fragments of First Order Logic, they are static in nature and are limited in what they can express from a temporal view point, hence the surge in temporal extensions to DLs over recent years. In this thesis we investigate the use of temporal extensions of DLs as suitable representations for the temporal information required for bio-health ontologies. We first set out to find out exactly what types of temporal information need to be modelled, before going on to evaluate current temporal extensions and representations to determine their suitability. We then go on to introduce several new temporal extensions to DLs and evaluate their suitability.

abstract: Robots are becoming an important part of our life and industry. Although a lot of robot control interfaces have been developed to simplify the control method and improve user experience, users still cannot control robots comfortably. With the improvements of the robot functions, the requirements of universality and ease of use of robot control interfaces are also increasing. This research introduces a graphical interface for Linear Temporal Logic (LTL) specifications for mobile robots. It is a sketch based interface built on the Android platform which makes the LTL control interface more friendly to non-expert users. By predefining a set of areas of interest, this interface can quickly and efficiently create plans that satisfy extended plan goals in LTL. The interface can also allow users to customize the paths for this plan by sketching a set of reference trajectories. Given the custom paths by the user, the LTL specification and the environment, the interface generates a plan balancing the customized paths and the LTL specifications. We also show experimental results with the implemented interface. / Dissertation/Thesis / Masters Thesis Computer Science 2016

abstract: In this thesis we deal with the problem of temporal logic robustness estimation. We present a dynamic programming algorithm for the robust estimation problem of Metric Temporal Logic (MTL) formulas regarding a finite trace of time stated sequence. This algorithm not only tests if the MTL specification is satisfied by the given input which is a finite system trajectory, but also quantifies to what extend does the sequence satisfies or violates the MTL specification. The implementation of the algorithm is the DP-TALIRO toolbox for MATLAB. Currently it is used as the temporal logic robust computing engine of S-TALIRO which is a tool for MATLAB searching for trajectories of minimal robustness in Simulink/ Stateflow. DP-TALIRO is expected to have near linear running time and constant memory requirement depending on the structure of the MTL formula. DP-TALIRO toolbox also integrates new features not supported in its ancestor FW-TALIRO such as parameter replacement, most related iteration and most related predicate. A derivative of DP-TALIRO which is DP-T-TALIRO is also addressed in this thesis which applies dynamic programming algorithm for time robustness computation. We test the running time of DP-TALIRO and compare it with FW-TALIRO. Finally, we present an application where DP-TALIRO is used as the robustness computation core of S-TALIRO for a parameter estimation problem. / Dissertation/Thesis / M.S. Computer Science 2013

This is the final revision of my M.Sc. Thesis. / Runtime Verification is a technique to extract information from a running system in order to detect executions violating a given correctness specification. In this thesis, we study distributed synchronous/asynchronous runtime verification of systems. In our setting, there is a set of distributed monitors that have only partial views of a large system and are subject to failures. In this context, it is unavoidable that monitors may have different views of the underlying system, and therefore may have different valuations of the correctness property. In this thesis, we propose an automata-based synchronous monitoring algorithm that copes with f crash failures in a distrbuted setting. The algorithm solves the synchronous monitoring problem in f + 1 rounds of communication, and significantly reduces the message size overhead. We also propose an algorithm for distributed crash-resilient asynchronous monitoring that consistently monitors the system under inspection without any communication between monitors. Each local monitor emits a verdict set solely based on its own partial observation, and the intersection of the verdict sets will be the same as the verdict computed by a centralized monitor that has full view of the system. / Thesis / Master of Science (MSc)