No description available.

No / Research studies report that there are a growing number of falsified educational certificates being produced by dishonest job seekers and higher education applicants across the world. Technological development in the image-processing domain makes editing the document so simple that any individual can perform this kind of forgery without having high-level skills in image editing. Most national governments have put in place stringent policies and procedures to verify and authenticate academic documents. However, due to the amount of human intervention in the process, the efficiency of such measures is debatable. Such systems leave open the possibility that unethical insiders may engage in forgery. In addition, the process of document verification and authentication consumes substantial amounts of time and money. Existing systems of document attestation do not provide a simple and instant way of verifying the authenticity of certificates from transcript level onward. In response to the above issues, this project proposes a prototype model for digitally managing and attesting the academic records using permissioned blockchain technology. By this method, the block-chaining of a student record begins from the time of admission to the Higher Education Institute (HEI) and continues to record the academic progress until graduation, having the graduation details stored as the last block in the chain. The whole blockchain of the student record will remain in the system with the participants enabling any indirect stakeholder to verify the details instantly based on the hash code or QR code. Additional privileges will be provided for direct stakeholders such as (here in Oman) the Ministry of Manpower and the Ministry of Higher Education to access further details of the certificate-holder. The system includes the student as a stakeholder and also as a participant to ensure transparency for her/his academic records.

In recent years, the number of exploits targeting software applications has increased dramatically. These exploits have caused substantial economic damages. Ensuring that software applications are not vulnerable to the exploits has, therefore, become a critical requirement. The last line of defense is to test before hand if a software application is vulnerable to exploits. One can accomplish this by testing for the presence of vulnerabilities. This dissertation presents a framework for deriving verification and validation (V&V) strategies to assess the security of a software application by testing it for the presence of vulnerabilities. This framework can be used to assess the security of any software application that executes above the level of the operating system. It affords a novel approach, which consists of testing if the software application permits violation of constraints imposed by computer system resources or assumptions made about the usage of these resources. A vulnerability exists if a constraint or an assumption can be violated. Distinctively different from other approaches found in the literature, this approach simplifies the process of assessing the security of a software application. The framework is composed of three components: (1) a taxonomy of vulnerabilities, which is an informative classification of vulnerabilities, where vulnerabilities are expressed in the form of violable constraints and assumptions; (2) an object model, which is a collection of potentially vulnerable process objects that can be present in a software application; and (3) a V&V strategies component, which combines information from the taxonomy and the object model; and provides approaches for testing software applications for the presence of vulnerabilities. This dissertation also presents a step-by-step process for using the framework to assess software security. / Ph. D.

This dissertation develops a modeling and simulation methodology for design, verification, and testing (DVT) power supply system using a virtual prototype. The virtual prototype is implemented before the hardware prototyping to detect most of the design errors and circuit deficiencies that occur in the later stage of a standard hardware design verification and testing procedure. The design iterations and product cost are reduced significantly by using this approach. The proposed modeling and simulation methodology consists of four major parts: system partitioning, multi-level modeling of device/function block, hierarchical test sequence, and multi-level simulation. By applying the proposed methodology, the designer can use the virtual prototype effectively by keeping a short simulation CPU time as well as catching most of the design problems. The proposed virtual prototype DVT procedure is demonstrated by simulating a 5 V power supply system with a main power supply, a bias power supply, and other protection, monitoring circuitry. The total CPU time is about 8 hours for 780 tests that include the basic function test, steady stage analysis, small-signal stability analysis, large-signal transient analysis, subsystem interaction test, and system interaction test. By comparing the simulation results with the measurements, it shows that the virtual prototype can represent the important behavior of the power supply system accurately. Since the proposed virtual prototype DVT procedure verifies the circuit design with different types of the tests over different line and load conditions, many circuit problems that are not obvious in the original circuit design can be detected by the simulation. The developed virtual prototype DVT procedure is not only capable of detecting most of the design errors, but also plays an important role in design modifications. This dissertation also demonstrates how to analyze the anomalies of the forward converter with active-clamp reset circuit extensively and facilitate the design and improve the circuit performances by utilizing the virtual prototype. With the help of the virtual prototype, it is the first time that the designer is able to analyze the dynamic behavior of the active-clamp forward converter during large-signal transient and optimize the design correspondingly. / Ph. D.

The most time-consuming component of designing and launching hardware products to market is the verification of Integrated Circuits (IC). An effective way of verifying a design can be achieved by adding assertions to the design. Automatic translation of hardware specifications from natural language to assertions in a formal representation has the potential to improve the verification productivity of ICs. However, natural language specifications have the characteristics of being imprecise, incomplete, and ambiguous. An automation framework can benefit verification engineers only if it is designed with the right balance between the ease of expression and precision of meaning allowed for in the input natural language specifications. This requirement introduces two major challenges for designing an effective translation framework. The first challenge is to allow the processing of expressive specifications with flexible word order variations and sentence structures. The second challenge is to assist users in writing unambiguous and complete specifications in the English language that can be accurately translated. In this dissertation, we address the first challenge by modeling semantic parsing of the input sentence as a game of BINGO that can capture the combinatorial nature of natural language semantics. BINGO parsing considers the context of each word in the input sentence to ensure high precision in the creation of semantic frames. We address the second challenge by designing a suggestion and feedback framework to assist users in writing clear and coherent specifications. Our feedback generates different ways of writing acceptable sentences when the input sentence is not understood. We evaluated our BINGO model on 316 hardware design specifications taken from the documents of AMBA, memory controller, and UART architectures. The results showed that highly expressive specifications could be handled in our BINGO model. It also demonstrated the ease of creating rules to generate the same semantic frame for specifications with the same meaning but different word order. We evaluated the suggestion and rewriting framework on 132 erroneous specifications taken from AMBA and memory controller architectures documents. Our system generated suggestions for all the specs. On manual inspection, we found that 87% of these suggestions were semantically closer to the intent of the input specification. Moreover, automatic contextual analysis of the rewritten form of the input specification allowed the translation of the input specification with different words and different order of words that were not defined in our grammar. / Doctor of Philosophy / The most time-consuming component of designing and launching hardware products to market is the verification of hardware circuits. An effective way of verifying a design is to add programming codes called assertions in the design. The creation of assertions can be time-consuming and error-prone due to the technical details needed to write assertions. Automatically translating assertion specifications written in English to program code can reduce design time and errors since the English language hides away the technical details required for writing assertions. However, sentences written in English language can have multiple and incomplete interpretations. It becomes difficult for machines to understand assertions written in the English language. In this work, we automatically generate assertions from assertion descriptions written in English. We propose techniques to write rules that can accurately translate English specifications to assertions. Our rules allow a user to write specifications with flexible use of word order and word interpretations. We have tested the understanding framework on English specifications taken from four different types of hardware design architectures. Since we cannot create rules to understand all possible ways of writing a specification, we have proposed a suggestion framework that can inform the user about the words and word structures acceptable to our translation framework. The suggestion framework was tested on specifications of AMBA and memory controller architectures.

Functional programming systems provide a number of features which facilitate program verification. Such verification may be observed to rest directly upon the theoretical foundations of computing and simultaneously to exhibit a close relation to the programs being verified. In order to demonstrate these aspects of functional systems, two functions, MIN and SORT, are defined on a parameterized type consisting of sequences to elements from some ordered type. Theorems showing that MIN and SORT terminate and return the correct values are stated and proved. Similar results are derived for a function to perform a binary search on an ordered sequence. Finally, conditions similar to Dijkstra’s weakest preconditions are given which allow the simultaneous synthesis and verification of certain programs from program specifications. A function to find the greatest common division of two integers is derived and verified. / M.S.

Routing metrics are important mechanisms to adjust routing protocols' path selection according to the needs of a network system. However, if a routing metric design does not correctly match a particular routing protocol, the protocol may not be able to find an optimal path; routing loops can be produced as well. Thus, the compatibility between routing metrics and routing protocols is increasingly significant with the widespread deployment of wired and wireless networks. However, it is usually difficult to tell whether a routing metric can be perfectly applied to a particular routing protocol. Manually enumerating all possible test cases is very challenging and often infeasible. Therefore, it is highly desirable to have an automatic solution so that one can avoid putting an incompatible combination of routing metric and protocol into use. In this thesis, the above issue has been addressed by developing two automated checking systems for examining the compatibility between real world routing metric and protocol implementations. The automatic routing protocol checking system assumes that some properties of routing metrics are given and the system's job is to check if a new routing protocol is able to achieve optimal, consistent and loop- free routing when it is combined with metrics that hold the given metric properties. In contrast to the protocol checking system, the automatic routing metric checking system assumes that a routing protocol is given and the checking system needs to verify if a new metric implementation will be able to work with this protocol. Experiments have been conducted to verify the correctness of both protocol and metric checking systems. / Master of Science

Massive GPS navigation services are used by billions of people in their daily lives. GPS spoofing is quite a challenging problem nowadays. Existing Anti-GPS spoofing systems primarily focus on expensive equipment and complicated algorithms, which are not practical and deployable for most of the users. In this thesis, we explore the feasibility of a simple text-based system design for Anti-GPS spoofing. The goal is to use the lower cost and make the system more effective and robust for general spoofing attack detection. Our key idea is to only use the textual information from the physical world and build a real-time system to detect GPS spoofing. To demonstrate the feasibility, we first design image processing modules to collect sufficient textual information in panoramic images. Then, we simulate real-world spoofing attacks from two cities to build our training and testing datasets. We utilize LSTM to build a binary classifier which is the key for our Anti-GPS spoofing system. Finally, we evaluate the system performance by simulating driving tests. We prove that our system can achieve more than 98% detection accuracy when the ratio of attacked points in a driving route is more than 50%. Our system has a promising performance for general spoofing attack strategies and it proves the feasibility of using textual information for the spoofing attack detection. / Master of Science / Nowadays, people are used to using GPS navigation services in their daily lives. However, GPS can be easily spoofed and the wrong GPS information will mislead victims to an unknown place. There are some existing methods that can defend GPS spoofing attacks, but all of them have significant shortcomings. Our goal is to design a novel system, which is cheap, effective, and robust, to detect general GPS spoofing attacks in real-time. In this thesis, we propose a complete system design and evaluations for performance. Our system only uses textual information from the real physical world and virtual maps. To get more accurate textual information, we use state of the art techniques for image processing and text recognition. We also use a neural network to help with detection. By testing with datasets in two cities, we confirm the promising performance of our system for general GPS spoofing attack strategies. We believe that textual information can be further developed in the Anti-GPS spoofing systems.

Yes / The complexity of pervasive systems arises from the many different aspects that such systems possess. A typical pervasive system may be autonomous, distributed, concurrent and context-based, and may involve humans and robotic devices working together. If we wish to formally verify the behaviour of such systems, the formal methods for pervasive systems will surely also be complex. In this paper, we move towards being able to formally verify pervasive systems and outline our approach wherein we distinguish four distinct dimensions within pervasive system behaviour and utilise different, but appropriate, formal techniques for verifying each one. / EPSRC

SMT-based verification analyzes reachability for transition systems represented by SMT formulae. Depending on the theories and the kinds of systems considered, various approaches have been proposed. Together, they form the Verification Modulo Theory (VMT) framework. This thesis delves into SMT-based verification of parameterized systems, emphasizing the challenges and novel solutions in verifying systems with an unbounded number of components. In this thesis, we first introduce a general framework to model such systems. Then, we introduce two novel algorithms that leverage the strengths of SMT for the verification of parameterized systems, focusing on the automation and reduction of computational complexity inherent in such tasks. These algorithms are designed to improve upon existing verification methods by offering enhanced scalability and automation, making them particularly suited for the analysis of distributed systems, network protocols, and concurrent programming models where traditional approaches may fail. Moreover, we introduce an algorithm for compositional verification that advances the capability to modularly verify complex systems by decomposing the verification task into smaller, more manageable sub-tasks. Additionally, we discuss the potential and ongoing application of these algorithms in an industrial project focusing on the design of interlocking logic. This particular application demonstrates the practical utility of our algorithms in a real-world setting, highlighting their effectiveness in improving the safety and reliability of critical infras- tructure. The theoretical advancements proposed in this thesis are complemented by a rig- orous experimental evaluation, demonstrating the applicability and effectiveness of our methods across a range of verification scenarios. Our work is implemented within an ex- tended framework of the MathSAT SMT solver, facilitating its integration into existing verification workflows. Overall, this research contributes to the theoretical underpinnings of Verification Modulo Theories (VMT) and offers tools and methodologies for the verification community, enhancing the capability to verify complex parameterized systems with greater efficiency and reliability.