Biblio

The fifth-generation (5G) standard is the last telecommunication technology, widely considered to have the most important characteristics in the future network industry. The 5G system infrastructure contains three principle interfaces, each one follows a set of protocols defined by the 3rd Generation Partnership Project group (3GPP). For the next generation network, 3GPP specified two authentication methods systematized in two protocols namely 5G Authentication and Key Agreement (5G-AKA) and Extensible Authentication Protocol (EAP). Such protocols are provided to ensure the authentication between system entities. These two protocols are critical systems, thus their reliability and correctness must be guaranteed. In this paper, we aim to formally re-examine 5G-AKA protocol using micro Common Representation Language 2 (mCRL2) language to verify such a security protocol. The mCRL2 language and its associated toolset are formal tools used for modeling, validation, and verification of concurrent systems and protocols. In this context, the authentication protocol 5G-AKA model is built using Algebra of Communication Processes (ACP), its properties are specified using Modal mu-Calculus and the properties analysis exploits Model-Checker provided with mCRL2. Indeed, we propose a new mCRL2 model of 3GPP specification considering 5G-AKA protocol and we specify some properties that describe necessary requirements to evaluate the correctness of the protocol where the parsed properties of Deadlock Freedom, Reachability, Liveness and Safety are positively assessed.

There are problems in which the use of linear regression is not sufficiently justified. In these cases, fuzzy linear regression can be used as a modeling tool. The problem of constructing a fuzzy linear regression can usually be reduced to a linear programming problem. One of the features of the resulting linear programming problem is that it uses a relatively large number of constraints in the form of inequalities with a relatively small number of variables. It is known that the problem of constructing a fuzzy linear regression is reduced to the problem of linear programming. If the user does not have enough computing power the resulting problem can be transferred to the cloud server. Two approaches are used for the confidential transfer of the problem to the server: the approach based on cryptographic encryption, and the transformational approach. The paper describes a protocol based on the transformational approach that allows for secure outsourcing of fuzzy linear regression.

The contemporary struggle that rests upon security risk assessment of Information Systems is its feasibility in the presence of an indeterminate environment when information is insufficient, conflicting, generic or ambiguous. But as pointed out by the security experts, most of the traditional approaches to risk assessment of information systems security are no longer practicable as they fail to deliver viable support on handling uncertainty. Therefore, to address this issue, we have anticipated a comprehensive risk assessment model based on Bayesian Belief Network (BBN) and Fuzzy Inference Scheme (FIS) process to function in an indeterminate environment. The proposed model is demonstrated and further comparisons are made on the test results to validate the reliability of the proposed model.

Phasor measurement units (PMUs) are used in power grids across North America to measure the amplitude, phase, and frequency of an alternating voltage or current. PMU's use the IEEE C37.118 protocol to send telemetry to phasor data collectors (PDC) and human machine interface (HMI) workstations in a control center. However, the C37.118 protocol utilizes the internet protocol stack without any authentication mechanism. This means that the protocol is vulnerable to false data injection (FDI) and false command injection (FCI). In order to study different scenarios in which C37.118 protocol's integrity and confidentiality can be compromised, we created a testbed that emulates a C37.118 communication network. In this testbed we conduct FCI and FDI attacks on real-time C37.118 data packets using a packet manipulation tool called Scapy. Using this platform, we generated C37.118 FCI and FDI datasets which are processed by multi-label machine learning classifier algorithms, such as Decision Tree (DT), k-Nearest Neighbor (kNN), and Naive Bayes (NB), to find out how effective machine learning can be at detecting such attacks. Our results show that the DT classifier had the best precision and recall rate.

With the world moving towards digitalization, more applications and servers are online hosted on the internet, more number of vulnerabilities came out which directly affects an individual and an organization financially and in terms of reputation too. Out of those many vulnerabilities such as Injection, Deserialization, Cross site scripting and more. Injection stand top as the most critical vulnerability found in the web application. Injection itself is a broad vulnerability as it further consists of SQL Injection, Command injection, LDAP Injection, No-SQL Injection etc. In this paper we have reviewed SQL Injection, different types of SQL injection attacks, their causes and remediation to comprehend this attack.

Android Operating System becomes a major target for malicious attacks. Static analysis approach is widely used to detect malicious applications. Most of existing studies on static analysis frameworks are limited to certain features. This paper presents an Android Static Analysis Framework (ASAF) which models the overall static analysis phases and approaches for Android applications. ASAF can be implemented for different purposes including Android malicious apps detection. The proposed framework utilizes a parsing tool, Android Static Parse (ASParse) which is also introduced in this paper. Through the extendibility of the ASParse tool, future research studies can easily extend the parsed features and the parsed files to perform parsing based on their specific requirements and goals. Moreover, a case study is conducted to illustrate the implementation of the proposed ASAF.

WebAssembly is a new W3C standard, providing a portable target for compilation for various languages. All major browsers can run WebAssembly programs, and its use extends beyond the web: there is interest in compiling cross-platform desktop applications, server applications, IoT and embedded applications to WebAssembly because of the performance and security guarantees it aims to provide. Indeed, WebAssembly has been carefully designed with security in mind. In particular, WebAssembly applications are sandboxed from their host environment. However, recent works have brought to light several limitations that expose WebAssembly to traditional attack vectors. Visitors of websites using WebAssembly have been exposed to malicious code as a result. In this paper, we propose an automated static program analysis to address these security concerns. Our analysis is focused on information flow and is compositional. For every WebAssembly function, it first computes a summary that describes in a sound manner where the information from its parameters and the global program state can flow to. These summaries can then be applied during the subsequent analysis of function calls. Through a classical fixed-point formulation, one obtains an approximation of the information flow in the WebAssembly program. This results in the first compositional static analysis for WebAssembly. On a set of 34 benchmark programs spanning 196kLOC of WebAssembly, we compute at least 64% of the function summaries precisely in less than a minute in total.

Software developers make mistakes that can lead to failures of a software product. One approach to detect defects is static analysis: examine code without execution. Currently, various source code static analysis tools are widely used to detect defects. However, source code analysis is not enough. The reason for this is the use of third-party binary libraries, the unprovability of the correctness of all compiler optimizations. This paper introduces BinSide : binary static analysis framework for defects detection. It does interprocedural, context-sensitive and flow-sensitive analysis. The framework uses platform independent intermediate representation and provide opportunity to analyze various architectures binaries. The framework includes value analysis, reaching definition, taint analysis, freed memory analysis, constant folding, and constant propagation engines. It provides API (application programming interface) and can be used to develop new analyzers. Additionally, we used the API to develop checkers for classic buffer overflow, format string, command injection, double free and use after free defects detection.

Web applications have become an essential resource to access the services of diverse subjects (e.g., financial, healthcare) available on the Internet. Despite the efforts that have been made on its security, namely on the investigation of better techniques to detect vulnerabilities on its source code, the number of vulnerabilities exploited has not decreased. Static analysis tools (SATs) are often used to test the security of applications since their outcomes can help developers in the correction of the bugs they found. The conducted investigation made over SATs stated they often generate errors (false positives (FP) and false negatives (FN)), whose cause is recurrently associated with very diverse coding styles, i.e., similar functionality is implemented in distinct manners, and programming practices that create ambiguity, such as the reuse and share of variables. Based on a common practice of using multiple forms in a same webpage and its processing in a single file, we defined a use case for user login and register with six coding styles scenarios for processing their data, and evaluated the behaviour of three SATs (phpSAFE, RIPS and WAP) with them to verify and understand why SATs produce FP and FN.

Due to the advantages and limitations of the two kinds of vulnerability mining methods of static and dynamic analysis of android applications, the paper proposes a method of Android application vulnerability mining based on dynamic and static combination. Firstly, the static analysis method is used to obtain the basic vulnerability analysis results of the application, and then the input test case of dynamic analysis is constructed on this basis. The fuzzy input test is carried out in the real machine environment, and the application security vulnerability is verified with the taint analysis technology, and finally the application vulnerability report is obtained. Experimental results show that compared with static analysis results, the method can significantly improve the accuracy of vulnerability mining.

The Android application market will conduct various security analysis on each application to predict its potential harm before put it online. Since almost all the static analysis tools can only detect malicious behaviors in the Java layer, more and more malwares try to avoid static analysis by taking the malicious codes to the Native layer. To provide a solution for the above situation, there's a new research aspect proposed in this paper and defined as Inter-language Static Analysis. As all the involved technologies are introduced, the current research results of them will be captured in this paper, such as static analysis in Java layer, binary analysis in Native layer, Java-Native penetration technology, etc.

As a modern power transmission network, smart grid connects abundant terminal devices and plays an important role in our daily life. However, along with its growth are the security threats. Different from the separated environment previously, an adversary nowadays can destroy the power system by attacking its terminal devices. As a result, it's critical to ensure the security and safety of terminal devices. To achieve it, detecting the pre-existing vulnerabilities in the terminal program and enhancing its security, are of great importance and necessity. In this paper, we introduce Cker, a novel vulnerability detection tool for smart grid devices, which generates an program model based on device sources and sets rules to perform model checking. We utilize the static analysis to extract necessary information and build corresponding program models. By further checking the model with pre-defined vulnerability patterns, we achieve security detection and error reporting. The evaluation results demonstrate that our method can effectively detect vulnerabilities in smart devices with an acceptable accuracy and false positive rate. In addition, as Cker is realized by pure python, it can be easily scaled to other platforms.

Fix pattern-based patch generation is a promising direction in Automated Program Repair (APR). Notably, it has been demonstrated to produce more acceptable and correct patches than the patches obtained with mutation operators through genetic programming. The performance of pattern-based APR systems, however, depends on the fix ingredients mined from fix changes in development histories. Unfortunately, collecting a reliable set of bug fixes in repositories can be challenging. In this paper, we propose to investigate the possibility in an APR scenario of leveraging code changes that address violations by static bug detection tools. To that end, we build the AVATAR APR system, which exploits fix patterns of static analysis violations as ingredients for patch generation. Evaluated on the Defects4J benchmark, we show that, assuming a perfect localization of faults, AVATAR can generate correct patches to fix 34/39 bugs. We further find that AVATAR yields performance metrics that are comparable to that of the closely-related approaches in the literature. While AVATAR outperforms many of the state-of-the-art pattern-based APR systems, it is mostly complementary to current approaches. Overall, our study highlights the relevance of static bug finding tools as indirect contributors of fix ingredients for addressing code defects identified with functional test cases.

Static analysis tools are programs that run on source code prior to their compilation to binary executables and attempt to find flaws or defects in the code during the early stages of development. If left unresolved, these flaws could pose security risks. While numerous static analysis tools exist, there is no single tool that is optimal. Therefore, many static analysis tools are often used to analyze code. Further, some of the alerts generated by the static analysis tools are low-priority or false alarms. Machine learning algorithms have been developed to distinguish between true alerts and false alarms, however significant man hours need to be dedicated to labeling data sets for training. This study investigates the use of active learning to reduce the number of labeled alerts needed to adequately train a classifier. The numerical experiments demonstrate that a query by committee active learning algorithm can be utilized to significantly reduce the number of labeled alerts needed to achieve similar performance as a classifier trained on a data set of nearly 60,000 labeled alerts.

Proofs in simulation-based frameworks have the greatest rigor when they are machine checked. But the level of details in these proofs surpasses what the formal-methods community can handle with existing tools. Existing formal results consider streamlined versions of simulation-based frameworks to cope with this complexity. Hence, a central question is how to abstract details from composability results and enable their formal verification.In this paper, we focus on the modeling of system communication in composable security statements. Existing formal models consider fixed communication patterns to reduce the complexity of their proofs. However, as we will show, this can affect the reusability of security statements. We propose an abstract approach to modeling system communication in Constructive Cryptography that avoids this problem. Our approach is suitable for mechanized verification and we use CryptHOL, a framework for developing mechanized cryptography proofs, to implement it in the Isabelle/HOL theorem prover. As a case study, we formalize the construction of a secure channel using Diffie-Hellman key exchange and a one-time-pad.

Fully Homomorphic Encryption (FHE) allows a third party to perform arbitrary computations on encrypted data, learning neither the inputs nor the computation results. Hence, it provides resilience in situations where computations are carried out by an untrusted or potentially compromised party. This powerful concept was first conceived by Rivest et al. in the 1970s. However, it remained unrealized until Craig Gentry presented the first feasible FHE scheme in 2009.The advent of the massive collection of sensitive data in cloud services, coupled with a plague of data breaches, moved highly regulated businesses to increasingly demand confidential and secure computing solutions. This demand, in turn, has led to a recent surge in the development of FHE tools. To understand the landscape of recent FHE tool developments, we conduct an extensive survey and experimental evaluation to explore the current state of the art and identify areas for future development.In this paper, we survey, evaluate, and systematize FHE tools and compilers. We perform experiments to evaluate these tools’ performance and usability aspects on a variety of applications. We conclude with recommendations for developers intending to develop FHE-based applications and a discussion on future directions for FHE tools development.

Modern SoC applications include a variety of sensitive modules in which data must be protected against malicious access. Security vulnerabilities, when exercised during the SoC operation, lead to denial of service or disclosure of protected data. Hence, it is essential to undertake security validation before and after SoC fabrication and make provisions for continuous security assessment during operation. This paper presents a methodology for optimized post-deployment monitoring of SoC's security properties by migrating pre-fab design security assertions to post-fab run-time security monitors. We show that the method is scalable for large systems and complex properties by optimizing the hardware monitors and applying it to a large SoC design based on a OpenRISC-1200 SoC. About 40 security assertions were specified in System Verilog Assertions (SVA). Following formal verification, the assertions were synthesized into finite state machines and cross optimized. Following code generation in Verilog, commercial logic and layout synthesis tools were used to generate hardware monitors which were then integrated with the SoC design ready for fabrication.

Human Resource (HR) Analytics has been increasingly attracted attention for a past decade. This is because the study field is adopted data-driven approaches to be processed and interpreted for meaningful insights in human resources. The field is involved in HR decision making helping to understand why people, organization, or other business performance behaved the way they do. Embracing the available tools for decision making and learning in the field of computational intelligence (CI) and Artificial Intelligence (AI) to the field of HR, this creates tremendous opportunities for HR Analytics in practical aspects. However, there are still inadequate applications in this area. This paper serves as a survey of using the tools and their applications in HR involving recruitment, retention, reward and retirement. An example of using CI and AI for career development and training in the era of disruption is conceptually proposed.

Safety- and security-critical developers have long recognized the importance of applying a high degree of scrutiny to a system’s (or subsystem’s) I/O messages. However, lack of care in the development of message-handling components can lead to an increase, rather than a decrease, in the attack surface. On the DARPA Cyber-Assured Systems Engineering (CASE) program, we have focused our research effort on identifying cyber vulnerabilities early in system development, in particular at the Architecture development phase, and then automatically synthesizing components that mitigate against the identified vulnerabilities from high-level specifications. This approach is highly compatible with the goals of the LangSec community. Advances in formal methods have allowed us to produce hardware/software implementations that are both performant and guaranteed correct. With these tools, we can synthesize high-assurance “building blocks” that can be composed automatically with high confidence to create trustworthy systems, using a method we call Security-Enhancing Architectural Transformations. Our synthesis-focused approach provides a higherleverage insertion point for formal methods than is possible with post facto analytic methods, as the formal methods tools directly contribute to the implementation of the system, without requiring developers to become formal methods experts. Our techniques encompass Systems, Hardware, and Software Development, as well as Hardware/Software Co-Design/CoAssurance. We illustrate our method and tools with an example that implements security-improving transformations on system architectures expressed using the Architecture Analysis and Design Language (AADL). We show how message-handling components can be synthesized from high-level regular or context-free language specifications, as well as a novel specification language for self-describing messages called Contiguity Types, and verified to meet arithmetic constraints extracted from the AADL model. Finally, we guarantee that the intent of the message processing logic is accurately reflected in the application binary code through the use of the verified CakeML compiler, in the case of software, or the Restricted Algorithmic C toolchain with ACL2-based formal verification, in the case of hardware/software co-design.

The software industry is dominating many are like health care, finance, agriculture and entertainment. Software security has become an essential issue-outsider libraries, which assume a significant part in programming. The finding weaknesses in the binary code is a significant issue that presently cannot seem to be handled, as showed by numerous weaknesses wrote about an everyday schedule. Software seller sells the software to the client if the client wants to check the software's vulnerability it is a cumbersome task. Presently many deep learning-based methods also introduced to find the security weakness in the binary code. This paper present the merits and demerits of binary code analysis used by a different method.

In the continuously evolving environment, computer security has become a convenient challenge because of the rapid rise and expansion of the Internet. One of the most significant challenges to networks is attacks on network resources caused by inadequate network security. DHCP is defenseless to a number of attacks, such as DHCP rogue server attacks. This work is focused on developing a method of detecting these attacks and granting active host protection on GNU/Linux operating systems. Unauthorized DHCP servers can be easily arranged and compete with the legitimate server on the local network that can be the result of distributing incorrect IP addresses, malicious DNS server addresses, invalid routing information to unsuspecting clients, intercepting and eavesdropping on communications, and so on. The goal is to prevent the situations described above by recognizing untrusted DHCP servers and providing active host protection on the local network.

Blockchain technology is the need of an hour for ensuring security and data privacy. However, very limited tools and documentation are available, therefore, the traditional code-centric implementation of Blockchain is challenging for programmers and developers due to inherent complexities. To overcome these challenges, in this article, a novel and efficient framework is proposed that is based on the Model-Driven Architecture. Particularly, a Meta-model (M2 level Ecore Model) is defined that contains the concepts of Blockchain technology. As a part of tool support, a tree editor (developed using Eclipse Modeling Framework) and a Sirius based graphical modeling tool with a drag-drop palette have been provided to allow modeling and visualization of simple and complex Blockchain-based scenarios for security labs in a very user-friendly manner. A Model to Text (M2T) transformation code has also been written using Acceleo language that transforms the modeled scenarios into java code for Blockchain application in the security lab. The validity of the proposed framework has been demonstrated via a case study. The results prove that our framework can be reliably used and further extended for automation and development of Blockchain-based application for security labs with simplicity.

{On considering workplace thefts as a major problem, there is a requirement of designing a vandal proof door hardware and locking mechanism for ensuring the security of our property. So the door lock system with extra security features with a user friendly cost is suggested in this paper. When a stranger comes at the door, he/she has to pass three security levels for unlocking the solenoid locks present at the door and if he fails to do so, the door will remain locked. These three levels are of three extraordinary security features as one of them is using Fingerprint sensor, second is using a knocking pattern, and the last lock is unlocked by the preset pin/pattern entered by the user. Since, in addition to these features, there is one more option for the case of appearing of guest at the door and that is the Image capturing using web-camera present at the door and here the owner of the house is able to unlock all the locks if he wants the guest to enter the home. This all will be monitored by Node MCU}.

Rapid development of wireless technologies has driven the evolution of smart grid application. In smart grid, authentication plays an important role for secure communication between smart meter and service provider. Hence, the design of secure authenticated key agreement schemes has received significant attention from researchers. In these schemes, a trusted third party directly participates in key agreement process. Although, this third party is assumed as trusted, however we cannot reject the possibility that being a third party, it can also be malicious. In the existing works, either the established session key is revealed to the agents of a trusted third party, or a trusted third party agent can impersonate the smart meter and establish a valid session key with the service provider, which is likely to cause security vulnerabilities. Therefore, there is a need to design a secure authentication scheme so that only the deserving entities involved in the communication can establish and know the session key. This paper proposes a new secure authenticated key agreement scheme for smart grid considering the fact that the third party can also be malicious. The security of the proposed scheme has been thoroughly evaluated using an adversary model. Correctness of the scheme has been analyzed using the broadly accepted Burrows-Abadi-Needham (BAN) Logic. In addition, the formal security verification of the proposed scheme has been performed using the widely accepted Automated Validation of Internet Security Protocols and Applications (AVISPA) simulation tool. Results of this simulation confirm that the proposed scheme is safe. Detailed security analysis shows the robustness of the scheme against various known attacks. Moreover, the comparative performance study of the proposed scheme with other relevant schemes is presented to demonstrate its practicality.

With the rapid development of the electric power Internet-of-Things (power IoT) technology and the widespread use of general-purpose software, hardware and network facilities, the power IoT has become more and more open, which makes the traditional power system face new cyber security threats. In order to find the vulnerable device nodes and attack links in the power IoT system, this paper studies a set of attack path calculation methods and vulnerability node discovery algorithms, which can construct a power IoT attack simulation program based on the value of equipment assets and information attributes. What’s more, this paper has carried on the example analysis and verification on the improved IEEE RBTS Bus 2 system. Based on the above research plan, this paper finally developed a set of power IoT attack simulation tool based on distribution electronic stations, which can well find the vulnerable devices in the system.