Biblio
Software verification has been well applied in safety critical areas and has shown the ability to provide better quality assurance for modern software. However, as lines of code and complexity of software systems increase, the scalability of verification becomes a challenge. In this paper, we present an automatic software verification framework TSV to address the scalability issues: (i) the extended structural abstraction and property-guided program slicing to solve large-scale program verification problem, saving time and memory without losing accuracy; (ii) automatically select different verification methods according to the program and property context to improve the verification efficiency. For evaluation, we compare TSV's different configurations with existing C program verifiers based on open benchmarks. We found that TSV with auto-selection performs better than with bounded model checking only or with extended structural abstraction only. Compared to existing tools such as CMBC and CPAChecker, it acquires 10%-20% improvement of accuracy and 50%-90% improvement of memory consumption.
Permissionless blockchains allow the execution of arbitrary programs (called smart contracts), enabling mutually untrusted entities to interact without relying on trusted third parties. Despite their potential, repeated security concerns have shaken the trust in handling billions of USD by smart contracts. To address this problem, we present Securify, a security analyzer for Ethereum smart contracts that is scalable, fully automated, and able to prove contract behaviors as safe/unsafe with respect to a given property. Securify's analysis consists of two steps. First, it symbolically analyzes the contract's dependency graph to extract precise semantic information from the code. Then, it checks compliance and violation patterns that capture sufficient conditions for proving if a property holds or not. To enable extensibility, all patterns are specified in a designated domain-specific language. Securify is publicly released, it has analyzed 18K contracts submitted by its users, and is regularly used to conduct security audits by experts. We present an extensive evaluation of Securify over real-world Ethereum smart contracts and demonstrate that it can effectively prove the correctness of smart contracts and discover critical violations.
GPUs have been widely used to accelerate big-data inference applications and scientific computing through their parallelized hardware resources and programming model. Their extreme parallelism increases the possibility of bugs such as data races and un-coalesced memory accesses, and thus verifying program correctness is critical. State-of-the-art GPU program verification efforts mainly focus on analyzing application-level programs, e.g., in C, and suffer from the following limitations: (1) high false-positive rate due to coarse-grained abstraction of synchronization primitives, (2) high complexity of reasoning about pointer arithmetic, and (3) keeping up with an evolving API for developing application-level programs. In this paper, we address these limitations by modeling GPUs and reasoning about programs at the instruction level. We formally model the Nvidia GPU at the parallel execution thread (PTX) level using the recently proposed Instruction-Level Abstraction (ILA) model for accelerators. PTX is analogous to the Instruction-Set Architecture (ISA) of a general-purpose processor. Our formal ILA model of the GPU includes non-synchronization instructions as well as all synchronization primitives, enabling us to verify multithreaded programs. We demonstrate the applicability of our ILA model in scalable GPU program verification of data-race checking. The evaluation shows that our checker outperforms state-of-the-art GPU data race checkers with fewer false-positives and improved scalability.
In this paper, we propose a new randomized response algorithm that can achieve differential-privacy and utility guarantees for consumer's behaviors, and process a batch of data at each time. Firstly, differing from traditional differential private approach-es, we add randomized response noise into the behavior signa-tures matrix to achieve an acceptable utility-privacy tradeoff. Secondly, a behavior signature modeling method based on sparse coding is proposed. After some lightweight trainings us-ing the energy consumption data, the dictionary will be associat-ed with the behavior characteristics of the electric appliances. At last, through the experimental results verification, we find that our Algorithm can preserve consumer's privacy without comprising utility.
Smart grids technologies are enablers of new business models for domestic consumers with local flexibility (generation, loads, storage) and where access to data is a key requirement in the value stream. However, legislation on personal data privacy and protection imposes the need to develop local models for flexibility modeling and forecasting and exchange models instead of personal data. This paper describes the functional architecture of an home energy management system (HEMS) and its optimization functions. A set of data-driven models, embedded in the HEMS, are discussed for improving renewable energy forecasting skill and modeling multi-period flexibility of distributed energy resources.
Recently a huge trend on the internet of things (IoT) and an exponential increase in automated tools are helping malware producers to target IoT devices. The traditional security solutions against malware are infeasible due to low computing power for large-scale data in IoT environment. The number of malware and their variants are increasing due to continuous malware attacks. Consequently, the performance improvement in malware analysis is critical requirement to stop rapid expansion of malicious attacks in IoT environment. To solve this problem, the paper proposed a novel framework for classifying malware in IoT environment. To achieve flne-grained malware classification in suggested framework, the malware image classification system (MICS) is designed for representing malware image globally and locally. MICS first converts the suspicious program into the gray-scale image and then captures hybrid local and global malware features to perform malware family classification. Preliminary experimental outcomes of MICS are quite promising with 97.4% classification accuracy on 9342 windows suspicious programs of 25 families. The experimental results indicate that proposed framework is quite capable to process large-scale IoT malware.
Certifying security controls is required for information systems that are either federally maintained or maintained by a US government contractor. As described in the NIST SP800-53, certified and accredited information systems are deployed with an acceptable security threat risk. Self-adaptive information systems that allow functional and decision-making changes to be dynamically configured at runtime may violate security controls increasing the risk of security threat to the system. Methods are needed to formalize the process of certification for security controls by expressing and verifying the functional and non-functional requirements to determine what risks are introduced through self-adaptation. We formally express the existence and behavior requirements of the mechanisms needed to guarantee the security controls' effectiveness using audit controls on program example. To reason over the risk of security control compliance given runtime self-adaptations, we use the KIV theorem prover on the functional requirements, extracting the verification concerns and workflow associated with the proof process. We augment the MAPE-K control loop planner with knowledge of the mechanisms that satisfy the existence criteria expressed by the security controls. We compare self-adaptive plans to assess their risk of security control violation prior to plan deployment.
The paper addresses the fundamental methodological problem of risk analysis and control in information technology (IT) – the definition of risk as a subject of interest. Based on analysis of many risk concepts, we provide a consistent definition that describes the phenomenon. The proposed terminology is sound in terms of system analysis principles and applicable to practical use in risk assessment and control. Implication to risk assessment methods were summarized.
The rapid development of mobile networks has revolutionized the way of accessing the Internet. The exponential growth of mobile subscribers, devices and various applications frequently brings about excessive traffic in mobile networks. The demand for higher data rates, lower latency and seamless handover further drive the demand for the improved mobile network design. However, traditional methods can no longer offer cost-efficient solutions for better user quality of experience with fast time-to-market. Recent work adopts SDN in LTE core networks to meet the requirement. In these software defined LTE core networks, scalability and security become important design issues that must be considered seriously. In this paper, we propose a scalable channel security scheme for the software defined LTE core network. It applies the VxLAN for scalable tunnel establishment and MACsec for security enhancement. According to our evaluation, the proposed scheme not only enhances the security of the channel communication between different network components, but also improves the flexibility and scalability of the core network with little performance penalty. Moreover, it can also shed light on the design of the next generation cellular network.
With the increase in the popularity of computerized online applications, the analysis, and detection of a growing number of newly discovered stealthy malware poses a significant challenge to the security community. Signature-based and behavior-based detection techniques are becoming inefficient in detecting new unknown malware. Machine learning solutions are employed to counter such intelligent malware and allow performing more comprehensive malware detection. This capability leads to an automatic analysis of malware behavior. The proposed oblique random forest ensemble learning technique is efficient for malware classification. The effectiveness of the proposed method is demonstrated with three malware classification datasets from various sources. The results are compared with other variants of decision tree learning models. The proposed system performs better than the existing system in terms of classification accuracy and false positive rate.
In recent years, deep convolution neural networks (DCNNs) have won many contests in machine learning, object detection, and pattern recognition. Furthermore, deep learning techniques achieved exceptional performance in image classification, reaching accuracy levels beyond human capability. Malware variants from similar categories often contain similarities due to code reuse. Converting malware samples into images can cause these patterns to manifest as image features, which can be exploited for DCNN classification. Techniques for converting malware binaries into images for visualization and classification have been reported in the literature, and while these methods do reach a high level of classification accuracy on training datasets, they tend to be vulnerable to overfitting and perform poorly on previously unseen samples. In this paper, we explore and document a variety of techniques for representing malware binaries as images with the goal of discovering a format best suited for deep learning. We implement a database for malware binaries from several families, stored in hexadecimal format. These malware samples are converted into images using various approaches and are used to train a neural network to recognize visual patterns in the input and classify malware based on the feature vectors. Each image type is assessed using a variety of learning models, such as transfer learning with existing DCNN architectures and feature extraction for support vector machine classifier training. Each technique is evaluated in terms of classification accuracy, result consistency, and time per trial. Our preliminary results indicate that improved image representation has the potential to enable more effective classification of new malware.
In this paper we propose a new algorithm to detect Advanced Persistent Threats (APT's) that relies on a graph model of HTTP traffic. We also implement a complete detection system with a web interface that allows to interactively analyze the data. We perform a complete parameter study and experimental evaluation using data collected on a real network. The results show that the performance of our system is comparable to currently available antiviruses, although antiviruses use signatures to detect known malwares while our algorithm solely uses behavior analysis to detect new undocumented attacks.
Mobile ad hoc networks (MANETs) are self-configuring, dynamic networks in which nodes are free to move. These nodes are susceptible to various malicious attacks. In this paper, we propose a distributed trust-based security scheme to prevent multiple attacks such as Probe, Denial-of-Service (DoS), Vampire, User-to-Root (U2R) occurring simultaneously. We report above 95% accuracy in data transmission and reception by applying the proposed scheme. The simulation has been carried out using network simulator ns-2 in a AODV routing protocol environment. To the best of the authors' knowledge, this is the first work reporting a distributed trust-based prevention scheme for preventing multiple attacks. We also check the scalability of the technique using variable node densities in the network.
With the growth of smartphone sales and app usage, fingerprinting and identification of smartphone apps have become a considerable threat to user security and privacy. Traffic analysis is one of the most common methods for identifying apps. Traditional countermeasures towards traffic analysis includes traffic morphing and multipath routing. The basic idea of multipath routing is to increase the difficulty for adversary to eavesdrop all traffic by splitting traffic into several subflows and transmitting them through different routes. Previous works in multipath routing mainly focus on Wireless Sensor Networks (WSNs) or Mobile Ad Hoc Networks (MANETs). In this paper, we propose a multipath routing scheme for smartphones with edge network assistance to mitigate traffic analysis attack. We consider an adversary with limited capability, that is, he can only intercept the traffic of one node following certain attack probability, and try to minimize the traffic an adversary can intercept. We formulate our design as a flow routing optimization problem. Then a heuristic algorithm is proposed to solve the problem. Finally, we present the simulation results for our scheme and justify that our scheme can effectively protect smartphones from traffic analysis attack.
With the progress over technology, it is becoming viable to set up mobile ad hoc networks for non-military services as like well. Examples consist of networks of cars, law about communication facilities into faraway areas, and exploiting the solidity between urban areas about present nodes such as cellular telephones according to offload or otherwise keep away from using base stations. In such networks, there is no strong motive according to assume as the nodes cooperate. Some nodes may also be disruptive and partial may additionally attempt according to save sources (e.g. battery power, memory, CPU cycles) through “selfish” behavior. The proposed method focuses on the robustness of packet forwarding: keeping the usual packet throughput over a mobile ad hoc network in the rear regarding nodes that misbehave at the routing layer. Proposed system listen at the routing layer or function no longer try after address attacks at lower layers (eg. jamming the network channel) and passive attacks kind of eavesdropping. Moreover such functionate now not bear together with issues kind of node authentication, securing routes, or message encryption. Proposed solution addresses an orthogonal problem the encouragement concerning proper routing participation.
In Mobile Ad-hoc Network (MANET), we cannot predict the clear picture of the topology of a node because of its varying nature. Without notice participation and departure of nodes results in lack of trust relationship between nodes. In such circumstances, there is no guarantee that path between two nodes would be secure or free of malicious nodes. The presence of single malicious node could lead repeatedly compromised node. After providing security to route and data packets still, there is a need for the implementation of defense mechanism that is intrusion detection system(IDS) against compromised nodes. In this paper, we have implemented IDS, which defend against some routing attacks like the black hole and gray hole successfully. After measuring performance we get marginally increased Packet delivery ratio and Throughput.
Hardware information flow analysis detects security vulnerabilities resulting from unintended design flaws, timing channels, and hardware Trojans. These information flow models are typically generated in a general way, which includes a significant amount of redundancy that is irrelevant to the specified security properties. In this work, we propose a property specific approach for information flow security. We create information flow models tailored to the properties to be verified by performing a property specific search to identify security critical paths. This helps find suspicious signals that require closer inspection and quickly eliminates portions of the design that are free of security violations. Our property specific trimming technique reduces the complexity of the security model; this accelerates security verification and restricts potential security violations to a smaller region which helps quickly pinpoint hardware security vulnerabilities.
A new approach of a formalism of hybrid automatons has been proposed for the analysis of conflict processes between the information system and the information's security malefactor. An example of probability-based assessment on malefactor's victory has been given and the possibility to abstract from a specific type of probability density function for the residence time of parties to the conflict in their possible states. A model of the distribution of destructive informational influences in the information system to connect the process of spread of destructive information processes and the process of changing subjects' states of the information system has been proposed. An example of the destructive information processes spread analysis has been given.
As security incidents might have disastrous consequences on an enterprise's information technology (IT), organizations need to secure their IT against threats. Threat intelligence (TI) promises to provide actionable information about current threats for information security management systems (ISMS). Common information range from malware characteristics to observed perpetrator origins that allow customizing security controls. The aim of this article is to assess the impact of utilizing public available threat feeds within the corporate process on an organization's security information level. We developed a framework to integrate TI for large corporations and evaluated said framework in cooperation with a global acting manufacturer and retailer. During the development of the TI framework, a specific provider of TI was analyzed and chosen for integration within the process of vulnerability management. The evaluation of this exemplary integration was assessed by members of the information security department at the cooperating enterprise. During our evaluation it was emphasized that a prioritization of management activities based on whether threats that have been observed in the wild are targeting them or similar companies. Furthermore, indicators of compromise (IoC) provided by the chosen TI source, can be automatically integrated utilizing a provided software development kit. Theoretical relevance is based on the contribution towards the verification of proposed benefits of TI integration, such as increasing the resilience of an enterprise network, within a real-world environment. Overall, practitioners suggest that TI integration should result in enhanced management of security budgets and more resilient enterprise networks.
Fuzzy extractors (Dodiset al., Eurocrypt 2004) turn a noisy secret into a stable, uniformly distributed key. Reusable fuzzy extractors remain secure when multiple keys are produced from a single noisy secret (Boyen, CCS 2004). Boyen showed information-theoretically secure reusable fuzzy extractors are subject to strong limitations. Simoens et al. (IEEE S&P, 2009) then showed deployed constructions suffer severe security breaks when reused. Canetti et al. (Eurocrypt 2016) used computational security to sidestep this problem, building a computationally secure reusable fuzzy extractor that corrects a sublinear fraction of errors. We introduce a generic approach to constructing reusable fuzzy extractors. We define a new primitive called a reusable pseudoentropic isometry that projects an input metric space to an output metric space. This projection preserves distance and entropy even if the same input is mapped to multiple output metric spaces. A reusable pseudoentropy isometry yields a reusable fuzzy extractor by 1) randomizing the noisy secret using the isometry and 2) applying a traditional fuzzy extractor to derive a secret key. We propose reusable pseudoentropic isometries for the set difference and Hamming metrics. The set difference construction is built from composable digital lockers (Canetti and Dakdouk, Eurocrypt 2008). For the Hamming metric, we show that the second construction of Canetti et al.(Eurocrypt 2016) can be seen as an instantiation of our framework. In both cases, the pseudoentropic isometry's reusability requires noisy secrets distributions to have entropy in each symbol of the alphabet. Our constructions yield the first reusable fuzzy extractors that correct a constant fraction of errors. We also implement our set difference solution and describe two use cases.
Industrial control systems (ICS) are key enabling systems that drive the productivity and efficiency of omnipresent industries such as power, gas, water treatment, transportation, and manufacturing. These systems consist of interconnected components that communicate over industrial networks using industrial protocols such as the Common Industrial Protocol (CIP). CIP is one of the most commonly used network-based process control protocols, and utilizes an object-oriented communication structure for device to device interaction. Due to this object-oriented structure, CIP communication reveals detailed information about the devices, the communication patterns, and the system, providing an in-depth view of the system. The details from this in-depth system perspective can be utilized as part of a system cybersecurity or discovery approach. However, due to the variety of commands, corresponding parameters, and variable layer structure of the CIP network layer, processing this layer is a challenging task. This paper presents a tool, Advanced CIP Evaluator (ACE), which passively processes the CIP communication layer and automatically extracts device, communication, and system information from observed network traffic. ACE was tested and verified using a representative ICS power generation testbed. Since ACE operates passively, without generating any network traffic of its own, system operations are not disturbed. This novel tool provides ICS information, such as networked devices, communication patterns, and system operation, at a depth and breadth that is unique compared with other known tools.
Insider threats pose a challenge to all companies and organizations. Identification of culprit after an attack is often too late and result in detrimental consequences for the organization. Majority of past research on insider threat has focused on post-hoc personality analysis of known insider threats to identify personality vulnerabilities. It has been proposed that certain personality vulnerabilities place individuals to be at risk to perpetuating insider threats should the environment and opportunity arise. To that end, this study utilizes a game-based approach to simulate a scenario of intellectual property theft and investigate behavioral and personality differences of individuals who exhibit insider-threat related behavior. Features were extracted from games, text collected through implicit and explicit measures, simultaneous facial expression recordings, and personality variables (HEXACO, Dark Triad and Entitlement Attitudes) calculated from questionnaire. We applied ensemble machine learning algorithms and show that they produce an acceptable balance of precision and recall. Our results showcase the possibility of harnessing personality variables, facial expressions and linguistic features in the modeling and prediction of insider-threat.
This paper demonstrates how the Insider Threat Cybersecurity Framework (ITCF) web tool and methodology help provide a more dynamic, defense-in-depth security posture against insider cyber and cyber-physical threats. ITCF includes over 30 cybersecurity best practices to help organizations identify, protect, detect, respond and recover to sophisticated insider threats and vulnerabilities. The paper tests the efficacy of this approach and helps validate and verify ITCF's capabilities and features through various insider attacks use-cases. Two case-studies were explored to determine how organizations can leverage ITCF to increase their overall security posture against insider attacks. The paper also highlights how ITCF facilitates implementation of the goals outlined in two Presidential Executive Orders to improve the security of classified information and help owners and operators secure critical infrastructure. In realization of these goals, ITCF: provides an easy to use rapid assessment tool to perform an insider threat self-assessment; determines the current insider threat cybersecurity posture; defines investment-based goals to achieve a target state; connects the cybersecurity posture with business processes, functions, and continuity; and finally, helps develop plans to answer critical organizational cybersecurity questions. In this paper, the webtool and its core capabilities are tested by performing an extensive comparative assessment over two different high-profile insider threat incidents.