Biblio
In VLSI industry the design cycle is categorized into Front End Design and Back End Design. Front End Design flow is from Specifications to functional verification of RTL design. Back End Design is from logic synthesis to fabrication of chip. Handheld devices like Mobile SOC's is an amalgamation of many components like GPU, camera, sensor, display etc. on one single chip. In order to integrate these components protocols are needed. One such protocol in the emerging trend is I3C protocol. I3C is abbreviated as Improved Inter Integrated Circuit developed by Mobile Industry Processor Interface (MIPI) alliance. Most probably used for the interconnection of sensors in Mobile SOC's. The main motivation of adapting the standard is for the increase speed and low pin count in most of the hardware chips. The bus protocol is backward compatible with I2C devices. The paper includes detailed study I3C bus protocol and developing verification environment for the protocol. The test bench environment is written and verified using system Verilog and UVM. The Universal Verification Methodology (UVM) is base class library built using System Verilog which provides the fundamental blocks needed to quickly develop reusable and well-constructed verification components and test environments. The Functional Coverage of around 93.55 % and Code Coverage of around 98.89 % is achieved by verification closure.
With the development of large scale integrated circuits, the functions of the IoT chips have been increasingly perfect. The verification work has become one of the most important aspects. On the one hand, an efficient verification platform can ensure the correctness of the design. On the other hand, it can shorten the chip design cycle and reduce the design cost. In this paper, based on a transmission protocol of the IoT node, we propose a verification method which combines simulation verification and FPGA-based prototype verification. We also constructed a system verification platform for the IoT smart node chip combining two kinds of verification above. We have simulated and verificatied the related functions of the node chip using this platform successfully. It has a great reference value.
For aerospace FPGA software products, traditional simulation method faces severe challenges to verify product requirements under complicated scenarios. Given the increasing maturity of formal verification technology, this method can significantly improve verification work efficiency and product design quality, by expanding coverage on those "blind spots" in product design which were not easily identified previously. Taking UART communication as an example, this paper proposes several critical points to use formal verification for asynchronous communication protocol. Experiments and practices indicate that formal verification for asynchronous communication protocol can effectively reduce the time required, ensure a complete verification process and more importantly, achieve more accurate and intuitive results.
With the growth of technology, designs became more complex and may contain bugs. This makes verification an indispensable part in product development. UVM describe a standard method for verification of designs which is reusable and portable. This paper verifies IIC bus protocol using Universal Verification Methodology. IIC controller is designed in Verilog using Vivado. It have APB interface and its function and code coverage is carried out in Mentor graphic Questasim 10.4e. This work achieved 83.87% code coverage and 91.11% functional coverage.
SDN (Software Defined Network) with multiple controllers draws more attention for the increasing scale of the network. The architecture can handle what SDN with single controller is not able to address. In order to understand what this architecture can accomplish and face precisely, we analyze it with formal methods. In this paper, we apply CSP (Communicating Sequential Processes) to model the routing service of SDN under HyperFlow architecture based on OpenFlow protocol. By using model checker PAT (Process Analysis Toolkit), we verify that the models satisfy three properties, covering deadlock freeness, consistency and fault tolerance.
As a decentralized and distributed secure storage technology, the notion of blockchain is now widely used for electronic trading in finance, for issuing digital certificates, for copyrights management, and for many other security-critical applications. With applications in so many domains with high-assurance requirements, the formalization and verification of safety and security properties of blockchain becomes essential, and the aim of the present paper. We present the model-based formalization, simulation and verification of a blockchain protocol by using the SDL formalism of Telelogic Tau. We consider the hierarchical and modular SDL model of the blockchain protocol and exercise a methodology to formally simulate and verify it. This way, we show how to effectively increase the security and safety of blockchain in order to meet high assurance requirements demanded by its application domains. Our work also provides effective support for assessing different network consensus algorithms, which are key components in blockchain protocols, as well as on the topology of blockchain networks. In conclusion, our approach contributes to setting up a verification methodology for future blockchain standards in digital trading.
Mobile communication networks connect much of the world's population. The security of users' calls, SMSs, and mobile data depends on the guarantees provided by the Authenticated Key Exchange protocols used. For the next-generation network (5G), the 3GPP group has standardized the 5G AKA protocol for this purpose. We provide the first comprehensive formal model of a protocol from the AKA family: 5G AKA. We also extract precise requirements from the 3GPP standards defining 5G and we identify missing security goals. Using the security protocol verification tool Tamarin, we conduct a full, systematic, security evaluation of the model with respect to the 5G security goals. Our automated analysis identifies the minimal security assumptions required for each security goal and we find that some critical security goals are not met, except under additional assumptions missing from the standard. Finally, we make explicit recommendations with provably secure fixes for the attacks and weaknesses we found.
We present the first formalisation of a blockchain-based distributed consensus protocol with a proof of its consistency mechanised in an interactive proof assistant. Our development includes a reference mechanisation of the block forest data structure, necessary for implementing provably correct per-node protocol logic. We also define a model of a network, implementing the protocol in the form of a replicated state-transition system. The protocol's executions are modeled via a small-step operational semantics for asynchronous message passing, in which packages can be rearranged or duplicated. In this work, we focus on the notion of global system safety, proving a form of eventual consistency. To do so, we provide a library of theorems about a pure functional implementation of block forests, define an inductive system invariant, and show that, in a quiescent system state, it implies a global agreement on the state of per-node transaction ledgers. Our development is parametric with respect to implementations of several security primitives, such as hash-functions, a notion of a proof object, a Validator Acceptance Function, and a Fork Choice Rule. We precisely characterise the assumptions, made about these components for proving the global system consensus, and discuss their adequacy. All results described in this paper are formalised in Coq.
This article describes a privacy policy framework that can represent and reason about complex privacy policies. By using a Common Data Model together with a formal shareability theory, this framework enables the specification of expressive policies in a concise way without burdening the user with technical details of the underlying formalism. We also build a privacy policy decision engine that implements the framework and that has been deployed as the policy decision point in a novel enterprise privacy prototype system. Our policy decision engine supports two main uses: (1) interfacing with user interfaces for the creation, validation, and management of privacy policies; and (2) interfacing with systems that manage data requests and replies by coordinating privacy policy engine decisions and access to (encrypted) databases using various privacy enhancing technologies.
Routers are important devices in the networks that carry the burden of transmitting information among the communication devices on the Internet. If a malicious adversary wants to intercept the information or paralyze the network, it can directly attack the routers and then achieve the suspicious goals. Thus, preventing router security is of great importance. However, router systems are notoriously difficult to understand or diagnose for their inaccessibility and heterogeneity. The common way of gaining access to the router system and detecting the anomaly behaviors is to inspect the router syslogs or monitor the packets of information flowing to the routers. These approaches just diagnose the routers from one aspect but do not consider them from multiple views. In this paper, we propose an approach to detect the anomalies and faults of the routers with multiple information learning. We try to use the routers' information not from the developer's view but from the user' s view, which does not need any expert knowledge. First, we do the offline learning to transform the benign or corrupted user actions into the syslogs. Then, we try to decide whether the input routers' conditions are poor or not with clustering. During the detection phase, we use the distance between the event and the cluster to decide if it is the anomaly event and we can provide the corresponding solutions. We have applied our approach in a university network which contains Cisco, Huawei and Dlink routers for three months. We aligned our experiment with former work as a baseline for comparison. Our approach can gain 89.6% accuracy in detecting the attacks which is 5.1% higher than the former work. The results show that our approach performs in limited time as well as memory usages and has high detection and low false positives.
Security research has made extensive use of exhaustive Internet-wide scans over the recent years, as they can provide significant insights into the overall state of security of the Internet, and ZMap made scanning the entire IPv4 address space practical. However, the IPv4 address space is exhausted, and a switch to IPv6, the only accepted long-term solution, is inevitable. In turn, to better understand the security of devices connected to the Internet, including in particular Internet of Things devices, it is imperative to include IPv6 addresses in security evaluations and scans. Unfortunately, it is practically infeasible to iterate through the entire IPv6 address space, as it is 2ˆ96 times larger than the IPv4 address space. Therefore, enumeration of active hosts prior to scanning is necessary. Without it, we will be unable to investigate the overall security of Internet-connected devices in the future. In this paper, we introduce a novel technique to enumerate an active part of the IPv6 address space by walking DNSSEC-signed IPv6 reverse zones. Subsequently, by scanning the enumerated addresses, we uncover significant security problems: the exposure of sensitive data, and incorrectly controlled access to hosts, such as access to routing infrastructure via administrative interfaces, all of which were accessible via IPv6. Furthermore, from our analysis of the differences between accessing dual-stack hosts via IPv6 and IPv4, we hypothesize that the root cause is that machines automatically and by default take on globally routable IPv6 addresses. This is a practice that the affected system administrators appear unaware of, as the respective services are almost always properly protected from unauthorized access via IPv4. Our findings indicate (i) that enumerating active IPv6 hosts is practical without a preferential network position contrary to common belief, (ii) that the security of active IPv6 hosts is currently still lagging behind the security state of IPv4 hosts, and (iii) that unintended IPv6 connectivity is a major security issue for unaware system administrators.
Many governments organizations in Libya have started transferring traditional government services to e-government. These e-services will benefit a wide range of public. However, deployment of e-government bring many new security issues. Attackers would take advantages of vulnerabilities in these e-services and would conduct cyber attacks that would result in data loss, services interruptions, privacy loss, financial loss, and other significant loss. The number of vulnerabilities in e-services have increase due to the complexity of the e-services system, a lack of secure programming practices, miss-configuration of systems and web applications vulnerabilities, or not staying up-to-date with security patches. Unfortunately, there is a lack of study being done to assess the current security level of Libyan government websites. Therefore, this study aims to assess the current security of 16 Libyan government websites using penetration testing framework. In this assessment, no exploits were committed or tried on the websites. In penetration testing framework (pen test), there are four main phases: Reconnaissance, Scanning, Enumeration, Vulnerability Assessment and, SSL encryption evaluation. The aim of a security assessment is to discover vulnerabilities that could be exploited by attackers. We also conducted a Content Analysis phase for all websites. In this phase, we searched for security and privacy policies implementation information on the government websites. The aim is to determine whether the websites are aware of current accepted standard for security and privacy. From our security assessment results of 16 Libyan government websites, we compared the websites based on the number of vulnerabilities found and the level of security policies. We only found 9 websites with high and medium vulnerabilities. Many of these vulnerabilities are due to outdated software and systems, miss-configuration of systems and not applying the latest security patches. These vulnerabilities could be used by cyber hackers to attack the systems and caused damages to the systems. Also, we found 5 websites didn't implement any SSL encryption for data transactions. Lastly, only 2 websites have published security and privacy policies on their websites. This seems to indicate that these websites were not concerned with current standard in security and privacy. Finally, we classify the 16 websites into 4 safety categories: highly unsafe, unsafe, somewhat unsafe and safe. We found only 1 website with a highly unsafe ranking. Based on our finding, we concluded that the security level of the Libyan government websites are adequate, but can be further improved. However, immediate actions need to be taken to mitigate possible cyber attacks by fixing the vulnerabilities and implementing SSL encryption. Also, the websites need to publish their security and privacy policy so the users could trust their websites.
Machine learning algorithms have reached mainstream status and are widely deployed in many applications. The accuracy of such algorithms depends significantly on the size of the underlying training dataset; in reality a small or medium sized organization often does not have enough data to train a reasonably accurate model. For such organizations, a realistic solution is to train machine learning models based on a joint dataset (which is a union of the individual ones). Unfortunately, privacy concerns prevent them from straightforwardly doing so. While a number of privacy-preserving solutions exist for collaborating organizations to securely aggregate the parameters in the process of training the models, we are not aware of any work that provides a rational framework for the participants to precisely balance the privacy loss and accuracy gain in their collaboration. In this paper, we model the collaborative training process as a two-player game where each player aims to achieve higher accuracy while preserving the privacy of its own dataset. We introduce the notion of Price of Privacy, a novel approach for measuring the impact of privacy protection on the accuracy in the proposed framework. Furthermore, we develop a game-theoretical model for different player types, and then either find or prove the existence of a Nash Equilibrium with regard to the strength of privacy protection for each player.
Control-hijacking attacks include code injection attacks and code reuse attacks. In recent years, with the emergence of the defense mechanism data-execution prevention(DEP), code reuse attacks have become mainstream, such as return-oriented programming(ROP), Jump-Oriented Programming(JOP), and Counterfeit Object-oriented Programming(COOP). And a series of defensive measures have been proposed, such as DEP, address space layout randomization (ASLR), coarse-grained Control-Flow Integrity(CFI) and fine-grained CFI. In this paper, we propose a new attack called function-oriented programming(FOP) to construct malicious program behavior. FOP takes advantage of the existing function of the C program to induce attack. We propose concrete algorithms for FOP gadgets and build a tool to identify FOP gadgets. FOP can successfully bypass coarse-grained CFI, and FOP also can bypass some existing fine-grained CFI technologies, such as shadow stack technology. We show a real-world attack for proftpd1.3.0 server in the Linux x64 environment. We believe that the FOP attack will encourage people to come up with more effective defense measures.
Securing Internet of things is a major concern as it deals with data that are personal, needed to be reliable, can direct and manipulate device decisions in a harmful way. Also regarding data generation process is heterogeneous, data being immense in volume, complex management. Quantum Computing and Internet of Things (IoT) coined as Quantum IoT defines a concept of greater security design which harness the virtue of quantum mechanics laws in Internet of Things (IoT) security management. Also it ensures secured data storage, processing, communication, data dynamics. In this paper, an IoT security infrastructure is introduced which is a hybrid one, with an extra layer, which ensures quantum state. This state prevents any sort of harmful actions from the eavesdroppers in the communication channel and cyber side, by maintaining its state, protecting the key by quantum cryptography BB84 protocol. An adapted version is introduced specific to this IoT scenario. A classical cryptography system `One-Time pad (OTP)' is used in the hybrid management. The novelty of this paper lies with the integration of classical and quantum communication for Internet of Things (IoT) security.
Since radio frequency identification (RFID) technology has been used in various scenarios such as supply chain, access control system and credit card, tremendous efforts have been made to improve the authentication between tags and readers to prevent potential attacks. Though effective in certain circumstances, these existing methods usually require a server to maintain a database of identity related information for every tag, which makes the system vulnerable to the SQL injection attack and not suitable for distributed environment. To address these problems, we now propose a novel blockchain-based mutual authentication security protocol. In this new scheme, there is no need for the trusted third parties to provide security and privacy for the system. Authentication is executed as an unmodifiable transaction based on blockchain rather than database, which applies to distributed RFID systems with high security demand and relatively low real-time requirement. Analysis shows that our protocol is logically correct and can prevent multiple attacks.
In this time of ubiquitous computing and the evolution of the Internet of Things (IoT), the deployment and development of Radio Frequency Identification (RFID) is becoming more extensive. Proving the simultaneous presence of a group of RFID tagged objects is a practical need in many application areas within the IoT domain. Security, privacy, and efficiency are central issues when designing such a grouping-proof protocol. This work is motivated by our serial-dependent and Sundaresan et al.'s grouping-proof protocols. In this paper, we propose a light, improved offline protocol: parallel-dependency grouping-proof protocol (PDGPP). The protocol focuses on security, privacy, and efficiency. PDGPP tackles the challenges of including robust privacy mechanisms and accommodates missing tags. It is scalable and complies with EPC C1G2.