As Internet of Things (IoT)-based systems become more prevalent in the era of data-driven intelligence, they are prone to some unprecedented challenges in terms of data security and systems scalability in an era of context-sensitive data. The current advances in IoT-driven data sensing and sharing rely on third-party sources of information (TTPs) that gather data from one party, then transmit it to the other. As a result of TTPs’ involvement, such IoT systems suffer from many issues including but not limited to security, transparency, trust, and immutability as a result of the involvement of the company. Moreover, a multitude of technical impediments, such as the computation and storage poverty of IoTs, privacy concerns, and energy efficiency, enhances the challenges for IoTs. To address these issues of IoT security, we propose a blockchain-enabled open IoT data-sharing framework based on the potential of the interplanetary file system (IPFS). We have used a case study-based approach to evaluate the proposed solution. It is submitted that the proposed scenario is implemented by building smart contracts in Solidity and deploying them on the local Ethereum test network, using the Solidity programming language. With the implementation of smart contracts on the blockchain for access roles in IoT data sensing, the proposed solution advocates for a blockchain-based approach to data security for IoT systems that makes use of smart contracts for access roles.

Cyber security confronts a tremendous challenge of maintaining the confidentiality and integrity of user’s private information such as password and PIN code. Billions of users are exposed daily to fake login pages requesting secret information. There are many ways to trick a user to visit a web page such as, phishing mails, tempting advertisements, click-jacking, malware, SQL injection, session hijacking, man-in-the-middle, denial of service and cross-site scripting attacks. Web spoofing or phishing is an electronic trick in which the attacker constructs a malicious copy of a legitimate web page and request users’ private information such as password. To counter such exploits, researchers have proposed several security strategies but they face latency and accuracy issues. To overcome such issues, we propose and develop client-side defence mechanism based on machine learning techniques to detect spoofed web pages and protect users from phishing attacks. As a proof of concept, a Google Chrome extension dubbed as PhishCatcher , is developed that implements our machine learning algorithm that classifies a URL as suspicious or trustful. The algorithm takes four different types of web features as input and then random forest classifier decides whether a login web page is spoofed or not. To assess the accuracy and precision of the extension, multiple experiments were carried on real web applications. The experimental results show remarkable accuracy of 98.5% and precision as 98.5% from the trials performed on 400 classified phished and 400 legitimate URLs. Furthermore, to measure the latency of our tool, we performed experiments over forty phished URLs. The average recorded response time of PhishCatcher was just 62.5 milliseconds.

Each software application running on Android powered devices consists of application components that communicate with each other to support application’s functionality for enhanced user experience of mobile computing. Application components inside Android system communicate with each other using inter-component communication mechanism based on messages called intents. An android application crashes if it invokes an intent that can not be received by (or resolved to) any application on the device. Application crashes represent a severe fault that relates to compromised users’ experience, consequently resulting in decreased ratings, usage trends and revenues for such applications. To address this issue—by formally proving crash-safety property of Android applications—we have defined a formal model of Android inter-component communication using Coq theorem prover. The mathematical model defined in theorem prover allows one to prove the properties of inter-component communication system and check the correctness of the proof in an automated way. To demonstrate the significance of the formal model developed, we carried proof of crash-safety of Android applications using Coq tool. The proposed solution named supports a formal approach that enables one to (i) check the correctness of inter-component communication in Android systems and (ii) establish a formal foundation for other tools to assess Android applications’ reliability and safety.

Hardware components, such as memory and arithmetic units, are integral part of every computer-controlled system, for example, Unmanned Aerial Vehicles (UAVs). The fundamental requirement of these hardware components is that they must behave as desired; otherwise, the whole system built upon them may fail. To determine whether or not a component is behaving adequately, the desired behaviour of the component is often specified in the Boolean algebra. Boolean algebra is one of the most widely used mathematical tools to analyse hardware components represented at gate level using Boolean functions. To ensure reliable computer-controlled system design, simulation and testing methods are commonly used to detect faults; however, such methods do not ensure absence of faults. In critical systems’ design, such as UAVs, the simulation-based techniques are often augmented with mathematical tools and techniques to prove stronger properties, for example, absence of faults, in the early stages of the system design. In this paper, we define a lightweight mathematical framework in computer-based theorem prover Coq for describing and reasoning about Boolean algebra and hardware components (logic circuits) modelled as Boolean functions. To demonstrate the usefulness of the framework, we (1) define and prove the correctness of principle of duality mechanically using a computer tool and all basic theorems of Boolean algebra, (2) formally define the algebraic manipulation (step-by-step procedure of proving functional equivalence of functions) used in Boolean function simplification, and (3) verify functional correctness and reliability properties of two hardware components. The major advantage of using mechanical theorem provers is that the correctness of all definitions and proofs can be checked mechanically using the type checker and proof checker facilities of the proof assistant Coq.

Mobile devices are an indispensable part of modern-day lives to support portable computations and context-aware communication. Android applications within a mobile device share data to support application operations and better user experience, which also increases security risks to device's data integrity and confidentiality. To analyze the security provided by the Android permissions, modern security techniques, based on the programming languages, have been used to enforce best practices for developing the secure Android applications. Android security assessment, based on the language-based techniques in an informal setting without formal tool support, is tedious and error-prone. Furthermore, the lack of proof of the soundness of the language-based techniques raises questions about the validity of the analysis. To enable computer-aided formal verification in Android security domain, we have developed a mathematical model of language-based Android security using computer-based proof assistant Coq. One of the main challenges for mechanizing the language-based security in theorem prover relates to the complexity of variable bindings in language-based security techniques. As the main contributions of the paper: 1) the language-based security, including variable binding, is formalized in theorem prover Coq; 2) a formal type checker is built to type check (capture safe data flows within) Android applications using computer; and 3) the soundness of the language-based security technique (type system) is mechanically verified. The formal model of the Android type system and their proof of soundness are machine-readable, and their correctness can be checked in the computer using Coq proof and type checkers.