Visible to the public Biblio

Found 1545 results

Filters: First Letter Of Title is S  [Clear All Filters]
Conference Paper
Sadasivam, G. K., Hota, C..  2015.  Scalable Honeypot Architecture for Identifying Malicious Network Activities. 2015 International Conference on Emerging Information Technology and Engineering Solutions. :27–31.

Server honey pots are computer systems that hide in a network capturing attack packets. As the name goes, server honey pots are installed in server machines running a set of services. Enterprises and government organisations deploy these honey pots to know the extent of attacks on their network. Since, most of the recent attacks are advanced persistent attacks there is much research work going on in building better peripheral security measures. In this paper, the authors have deployed several honey pots in a virtualized environment to gather traces of malicious activities. The network infrastructure is resilient and provides much information about hacker's activities. It is cost-effective and can be easily deployed in any organisation without specialized hardware.

Takita, Yutaka, Miyabe, Masatake, Tomonaga, Hiroshi, Oguchi, Naoki.  2020.  Scalable Impact Range Detection against Newly Added Rules for Smart Network Verification. 2020 IEEE 44th Annual Computers, Software, and Applications Conference (COMPSAC). :1471–1476.
Technological progress in cloud networking, 5G networks, and the IoT (Internet of Things) are remarkable. In addition, demands for flexible construction of SoEs (Systems on Engagement) for various type of businesses are increasing. In such environments, dynamic changes of network rules, such as access control (AC) or packet forwarding, are required to ensure function and security in networks. On the other hand, it is becoming increasingly difficult to grasp the exact situation in such networks by utilizing current well-known network verification technologies since a huge number of network rules are complexly intertwined. To mitigate these issues, we have proposed a scalable network verification approach utilizing the concept of "Packet Equivalence Class (PEC)," which enable precise network function verification by strictly recognizing the impact range of each network rule. However, this approach is still not scalable for very large-scale networks which consist of tens of thousands of routers. In this paper, we enhanced our impact range detection algorithm for practical large-scale networks. Through evaluation in the network with more than 80,000 AC rules, we confirmed that our enhanced algorithm can achieve precise impact range detection in under 600 seconds.
Lin, Xiaofeng, Chen, Yu, Li, Xiaodong, Mao, Junjie, He, Jiaquan, Xu, Wei, Shi, Yuanchun.  2016.  Scalable Kernel TCP Design and Implementation for Short-Lived Connections. Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems. :339–352.

With the rapid growth of network bandwidth, increases in CPU cores on a single machine, and application API models demanding more short-lived connections, a scalable TCP stack is performance-critical. Although many clean-state designs have been proposed, production environments still call for a bottom-up parallel TCP stack design that is backward-compatible with existing applications. We present Fastsocket, a BSD Socket-compatible and scalable kernel socket design, which achieves table-level connection partition in TCP stack and guarantees connection locality for both passive and active connections. Fastsocket architecture is a ground up partition design, from NIC interrupts all the way up to applications, which naturally eliminates various lock contentions in the entire stack. Moreover, Fastsocket maintains the full functionality of the kernel TCP stack and BSD-socket-compatible API, and thus applications need no modifications. Our evaluations show that Fastsocket achieves a speedup of 20.4x on a 24-core machine under a workload of short-lived connections, outperforming the state-of-the-art Linux kernel TCP implementations. When scaling up to 24 CPU cores, Fastsocket increases the throughput of Nginx and HAProxy by 267% and 621% respectively compared with the base Linux kernel. We also demonstrate that Fastsocket can achieve scalability and preserve BSD socket API at the same time. Fastsocket is already deployed in the production environment of Sina WeiBo, serving 50 million daily active users and billions of requests per day.

Zhang, Xuyun, Leckie, Christopher, Dou, Wanchun, Chen, Jinjun, Kotagiri, Ramamohanarao, Salcic, Zoran.  2016.  Scalable Local-Recoding Anonymization Using Locality Sensitive Hashing for Big Data Privacy Preservation. Proceedings of the 25th ACM International on Conference on Information and Knowledge Management. :1793–1802.

While cloud computing has become an attractive platform for supporting data intensive applications, a major obstacle to the adoption of cloud computing in sectors such as health and defense is the privacy risk associated with releasing datasets to third-parties in the cloud for analysis. A widely-adopted technique for data privacy preservation is to anonymize data via local recoding. However, most existing local-recoding techniques are either serial or distributed without directly optimizing scalability, thus rendering them unsuitable for big data applications. In this paper, we propose a highly scalable approach to local-recoding anonymization in cloud computing, based on Locality Sensitive Hashing (LSH). Specifically, a novel semantic distance metric is presented for use with LSH to measure the similarity between two data records. Then, LSH with the MinHash function family can be employed to divide datasets into multiple partitions for use with MapReduce to parallelize computation while preserving similarity. By using our efficient LSH-based scheme, we can anonymize each partition through the use of a recursive agglomerative \$k\$-member clustering algorithm. Extensive experiments on real-life datasets show that our approach significantly improves the scalability and time-efficiency of local-recoding anonymization by orders of magnitude over existing approaches.

Yang, B., Zhang, T..  2016.  A Scalable Meta-Model for Big Data Security Analyses. 2016 IEEE 2nd International Conference on Big Data Security on Cloud (BigDataSecurity), IEEE International Conference on High Performance and Smart Computing (HPSC), and IEEE International Conference on Intelligent Data and Security (IDS). :55–60.

This paper proposes a highly scalable framework that can be applied to detect network anomaly at per flow level by constructing a meta-model for a family of machine learning algorithms or statistical data models. The approach is scalable and attainable because raw data needs to be accessed only one time and it will be processed, computed and transformed into a meta-model matrix in a much smaller size that can be resident in the system RAM. The calculation of meta-model matrix can be achieved through disposable updating operations at per row level: once a per-flow information is proceeded, it is no longer needed in calculating the meta-model matrix. While the proposed framework covers both Gaussian and non-Gaussian data, the focus of this work is on the linear regression models. Specifically, a new concept called meta-model sufficient statistics is proposed to analyze a group of models, where exact, not the approximate, results are derived. In addition, the proposed framework can quickly discover an optimal statistical or computer model from a family of candidate models without the need of rescanning the raw dataset. This suggest an extremely efficient and effectively theory and method is possible for big data security analysis.

Zelenbaba, Stefan, Löschenbrand, David, Hofer, Markus, Dakić, Anja, Rainer, Benjamin, Humer, Gerhard, Zemen, Thomas.  2020.  A Scalable Mobile Multi-Node Channel Sounder. 2020 IEEE Wireless Communications and Networking Conference (WCNC). :1—6.

The advantages of measuring multiple wireless links simultaneously has been gaining attention due to the growing complexity of wireless communication systems. Analyzing vehicular communication systems presents a particular challenge due to their rapid time-varying nature. Therefore multi-node channel sounding is crucial for such endeavors. In this paper, we present the architecture and practical implementation of a scalable mobile multi-node channel sounder, optimized for use in vehicular scenarios. We perform a measurement campaign with three moving nodes, which includes a line of sight (LoS) connection on two links and non LoS(NLoS) conditions on the third link. We present the results on the obtained channel delay and Doppler characteristics, followed by the assessment of the degree of correlation of the analyzed channels and time-variant channel rates, hence investigating the suitability of the channel's physical attributes for relaying. The results show low cross-correlation between the transfer functions of the direct and the relaying link, while a higher rate is calculated for the relaying link.

Ulrich, Jacob, McJunkin, Timothy, Rieger, Craig, Runyon, Michael.  2020.  Scalable, Physical Effects Measurable Microgrid for Cyber Resilience Analysis (SPEMMCRA). 2020 Resilience Week (RWS). :194—201.

The ability to advance the state of the art in automated cybersecurity protections for industrial control systems (ICS) has as a prerequisite of understanding the trade-off space. That is, to enable a cyber feedback loop in a control system environment you must first consider both the security mitigation available, the benefits and the impacts to the control system functionality when the mitigation is used. More damaging impacts could be precipitated that the mitigation was intended to rectify. This paper details networked ICS that controls a simulation of the frequency response represented with the swing equation. The microgrid loads and base generation can be balanced through the control of an emulated battery and power inverter. The simulated plant, which is implemented in Raspberry Pi computers, provides an inexpensive platform to realize the physical effects of cyber attacks to show the trade-offs of available mitigating actions. This network design can include a commercial ICS controller and simple plant or emulated plant to introduce real world implementation of feedback controls, and provides a scalable, physical effects measurable microgrid for cyber resilience analysis (SPEMMCRA).

Adelt, Peer, Koppelmann, Bastian, Mueller, Wolfgang, Scheytt, Christoph.  2020.  A Scalable Platform for QEMU Based Fault Effect Analysis for RISC-V Hardware Architectures. MBMV 2020 - Methods and Description Languages for Modelling and Verification of Circuits and Systems; GMM/ITG/GI-Workshop. :1–8.
Fault effect simulation is a well-established technique for the qualification of robust embedded software and hardware as required by different safety standards. Our article introduces a Virtual Prototype based approach for the fault analysis and fast simulation of a set of automatically generated and target compiled software programs. The approach scales to different RISC-V ISA standard subset configurations and is based on an instruction and hardware register coverage for automatic fault injections of permanent and transient bitflips. The analysis of each software binary evaluates its opcode type and register access coverage including the addressed memory space. Based on this information dedicated sets of fault injected hardware models, i.e., mutants, are generated. The simulation of all mutants conducted with the different binaries finally identifies the cases with a normal termination though executed on a faulty hardware model. They are identified as a subject for further investigations and improvements by the implementation of additional hardware or software safety countermeasures. Our final evaluation results with automatic C code generation, compilation, analysis, and simulation show that QEMU provides an adequate efficient platform, which also scales to more complex scenarios.
Rosa, Taras, Kaidan, Mykola, Gazda, Juraj, Bykovyy, Pavlo, Sapozhnyk, Grygoriy, Maksymyuk, Taras.  2019.  Scalable QAM Modulation for Physical Layer Security of Wireless Networks. 2019 10th IEEE International Conference on Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications (IDAACS). 2:1095–1098.
The rapid growth of the connected devices driven by Internet of Things (IoT) concept requires a complete rethinking of the conventional approaches for the network design. One of the key constraints of the IoT devices are their low capabilities in order to optimize energy consumption. On the other hand, many IoT applications require high level of data protection and privacy, which can be provided only by advanced cryptographic algorithms, which are not feasible for IoT devices. In this paper, we propose a scalable quadrature modulation aiming to solve the problem of secure communications at the physical layer. The key idea of the proposed approach is to transmit only part of information in way that allows target receiver to retrieve the complete information. Such approach allows to ensure the security of wireless channel, while reducing the overhead of advanced cryptographic algorithms.
Hamad, R. M. H., Fayoumi, M. Al.  2019.  Scalable Quality and Testing Lab (SQTL): Mission-Critical Applications Testing. 2019 International Conference on Computer and Information Sciences (ICCIS). :1–7.

Currently, the complexity of software quality and testing is increasing exponentially with a huge number of challenges knocking doors, especially when testing a mission-critical application in banking and other critical domains, or the new technology trends with decentralized and nonintegrated testing tools. From practical experience, software testing has become costly and more effort-intensive with unlimited scope. This thesis promotes the Scalable Quality and Testing Lab (SQTL), it's a centralized quality and testing platform, which integrates a powerful manual, automation and business intelligence tools. SQTL helps quality engineers (QE) effectively organize, manage and control all testing activities in one centralized lab, starting from creating test cases, then executing different testing types such as web, security and others. And finally, ending with analyzing and displaying all testing activities result in an interactive dashboard, which allows QE to forecast new bugs especially those related to security. The centralized SQTL is to empower QE during the testing cycle, help them to achieve a greater level of software quality in minimum time, effort and cost, and decrease defect density metric.

Huyn, Joojay.  2017.  A Scalable Real-Time Framework for DDoS Traffic Monitoring and Characterization. Proceedings of the Fourth IEEE/ACM International Conference on Big Data Computing, Applications and Technologies. :265–266.

Volumetric DDoS attacks continue to inflict serious damage. Many proposed defenses for mitigating such attacks assume that a monitoring system has already detected the attack. However, many proposed DDoS monitoring systems do not focus on efficiently analyzing high volume network traffic to provide important characterizations of the attack in real-time to downstream traffic filtering systems. We propose a scalable real-time framework for an effective volumetric DDoS monitoring system that leverages modern big data technologies for streaming analytics of high volume network traffic to accurately detect and characterize attacks.

Pawar, Shrikant, Stanam, Aditya.  2020.  Scalable, Reliable and Robust Data Mining Infrastructures. 2020 Fourth World Conference on Smart Trends in Systems, Security and Sustainability (WorldS4). :123—125.

Mining of data is used to analyze facts to discover formerly unknown patterns, classifying and grouping the records. There are several crucial scalable statistics mining platforms that have been developed in latest years. RapidMiner is a famous open source software which can be used for advanced analytics, Weka and Orange are important tools of machine learning for classifying patterns with techniques of clustering and regression, whilst Knime is often used for facts preprocessing like information extraction, transformation and loading. This article encapsulates the most important and robust platforms.

Camenisch, Jan, Drijvers, Manu, Hajny, Jan.  2016.  Scalable Revocation Scheme for Anonymous Credentials Based on N-times Unlinkable Proofs. Proceedings of the 2016 ACM on Workshop on Privacy in the Electronic Society. :123–133.

We propose the first verifier-local revocation scheme for privacy-enhancing attribute-based credentials (PABCs) that is practically usable in large-scale applications, such as national eID cards, public transportation and physical access control systems. By using our revocation scheme together with existing PABCs, it is possible to prove attribute ownership in constant time and verify the proof and the revocation status in the time logarithmic in the number of revoked users, independently of the number of all valid users in the system. Proofs can be efficiently generated using only offline constrained devices, such as existing smart-cards. These features are achieved by using a new construction called \$n\$-times unlinkable proofs. We show the full cryptographic description of the scheme, prove its security, discuss parameters influencing scalability and provide details on implementation aspects. As a side result of independent interest, we design a more efficient proof of knowledge of weak Boneh-Boyen signatures, that does not require any pairing computation on the prover side.

Yavari, A., Panah, A. S., Georgakopoulos, D., Jayaraman, P. P., Schyndel, R. v.  2017.  Scalable Role-Based Data Disclosure Control for the Internet of Things. 2017 IEEE 37th International Conference on Distributed Computing Systems (ICDCS). :2226–2233.

The Internet of Things (IoT) is the latest Internet evolution that interconnects billions of devices, such as cameras, sensors, RFIDs, smart phones, wearable devices, ODBII dongles, etc. Federations of such IoT devices (or things) provides the information needed to solve many important problems that have been too difficult to harness before. Despite these great benefits, privacy in IoT remains a great concern, in particular when the number of things increases. This presses the need for the development of highly scalable and computationally efficient mechanisms to prevent unauthorised access and disclosure of sensitive information generated by things. In this paper, we address this need by proposing a lightweight, yet highly scalable, data obfuscation technique. For this purpose, a digital watermarking technique is used to control perturbation of sensitive data that enables legitimate users to de-obfuscate perturbed data. To enhance the scalability of our solution, we also introduce a contextualisation service that achieve real-time aggregation and filtering of IoT data for large number of designated users. We, then, assess the effectiveness of the proposed technique by considering a health-care scenario that involves data streamed from various wearable and stationary sensors capturing health data, such as heart-rate and blood pressure. An analysis of the experimental results that illustrate the unconstrained scalability of our technique concludes the paper.

Kim, J., Moon, I., Lee, K., Suh, S. C., Kim, I..  2015.  Scalable Security Event Aggregation for Situation Analysis. 2015 IEEE First International Conference on Big Data Computing Service and Applications. :14–23.

Cyber-attacks have been evolved in a way to be more sophisticated by employing combinations of attack methodologies with greater impacts. For instance, Advanced Persistent Threats (APTs) employ a set of stealthy hacking processes running over a long period of time, making it much hard to detect. With this trend, the importance of big-data security analytics has taken greater attention since identifying such latest attacks requires large-scale data processing and analysis. In this paper, we present SEAS-MR (Security Event Aggregation System over MapReduce) that facilitates scalable security event aggregation for comprehensive situation analysis. The introduced system provides the following three core functions: (i) periodic aggregation, (ii) on-demand aggregation, and (iii) query support for effective analysis. We describe our design and implementation of the system over MapReduce and high-level query languages, and report our experimental results collected through extensive settings on a Hadoop cluster for performance evaluation and design impacts.

J. Kim, I. Moon, K. Lee, S. C. Suh, I. Kim.  2015.  "Scalable Security Event Aggregation for Situation Analysis". 2015 IEEE First International Conference on Big Data Computing Service and Applications. :14-23.

Cyber-attacks have been evolved in a way to be more sophisticated by employing combinations of attack methodologies with greater impacts. For instance, Advanced Persistent Threats (APTs) employ a set of stealthy hacking processes running over a long period of time, making it much hard to detect. With this trend, the importance of big-data security analytics has taken greater attention since identifying such latest attacks requires large-scale data processing and analysis. In this paper, we present SEAS-MR (Security Event Aggregation System over MapReduce) that facilitates scalable security event aggregation for comprehensive situation analysis. The introduced system provides the following three core functions: (i) periodic aggregation, (ii) on-demand aggregation, and (iii) query support for effective analysis. We describe our design and implementation of the system over MapReduce and high-level query languages, and report our experimental results collected through extensive settings on a Hadoop cluster for performance evaluation and design impacts.

Hong, J.B., Dong Seong Kim.  2014.  Scalable Security Models for Assessing Effectiveness of Moving Target Defenses. Dependable Systems and Networks (DSN), 2014 44th Annual IEEE/IFIP International Conference on. :515-526.

Moving Target Defense (MTD) changes the attack surface of a system that confuses intruders to thwart attacks. Various MTD techniques are developed to enhance the security of a networked system, but the effectiveness of these techniques is not well assessed. Security models (e.g., Attack Graphs (AGs)) provide formal methods of assessing security, but modeling the MTD techniques in security models has not been studied. In this paper, we incorporate the MTD techniques in security modeling and analysis using a scalable security model, namely Hierarchical Attack Representation Models (HARMs), to assess the effectiveness of the MTD techniques. In addition, we use importance measures (IMs) for scalable security analysis and deploying the MTD techniques in an effective manner. The performance comparison between the HARM and the AG is given. Also, we compare the performance of using the IMs and the exhaustive search method in simulations.

Goli, Mehran, Drechsler, Rolf.  2019.  Scalable Simulation-Based Verification of SystemC-Based Virtual Prototypes. 2019 22nd Euromicro Conference on Digital System Design (DSD). :522–529.
Virtual Prototypes (VPs) at the Electronic System Level (ESL) written in SystemC language using its Transaction Level Modeling (TLM) framework are increasingly adopted by the semiconductor industry. The main reason is that VPs are much earlier available, and their simulation is orders of magnitude faster in comparison to the hardware models implemented at lower levels of abstraction (e.g. RTL). This leads designers to use VPs as reference models for an early design verification. Hence, the correctness assurance of these reference models (VPs) is critical as undetected faults may propagate to less abstract levels in the design process, increasing the fixing cost and effort. In this paper, we propose a novel simulation-based verification approach to automatically validate the simulation behavior of a given SystemC VP against both the TLM-2.0 rules and its specifications (i.e. functional and timing behavior of communications in the VP). The scalability and the efficiency of the proposed approach are demonstrated using an extensive set of experiments including a real-word VP.
Gauthier, F., Keynes, N., Allen, N., Corney, D., Krishnan, P..  2018.  Scalable Static Analysis to Detect Security Vulnerabilities: Challenges and Solutions. 2018 IEEE Cybersecurity Development (SecDev). :134-134.

Parfait [1] is a static analysis tool originally developed to find implementation defects in C/C++ systems code. Parfait's focus is on proving both high precision (low false positives) as well as scaling to systems with millions of lines of code (typically requiring 10 minutes of analysis time per million lines). Parfait has since been extended to detect security vulnerabilities in applications code, supporting the Java EE and PL/SQL server stack. In this abstract we describe some of the challenges we encountered in this process including some of the differences seen between the applications code being analysed, our solutions that enable us to analyse a variety of applications, and a summary of the challenges that remain.

Sim, H., Nguyen, D., Lee, J., Choi, K..  2017.  Scalable stochastic-computing accelerator for convolutional neural networks. 2017 22nd Asia and South Pacific Design Automation Conference (ASP-DAC). :696–701.

Stochastic Computing (SC) is an alternative design paradigm particularly useful for applications where cost is critical. SC has been applied to neural networks, as neural networks are known for their high computational complexity. However previous work in this area has critical limitations such as the fully-parallel architecture assumption, which prevent them from being applicable to recent ones such as convolutional neural networks, or ConvNets. This paper presents the first SC architecture for ConvNets, shows its feasibility, with detailed analyses of implementation overheads. Our SC-ConvNet is a hybrid between SC and conventional binary design, which is a marked difference from earlier SC-based neural networks. Though this might seem like a compromise, it is a novel feature driven by the need to support modern ConvNets at scale, which commonly have many, large layers. Our proposed architecture also features hybrid layer composition, which helps achieve very high recognition accuracy. Our detailed evaluation results involving functional simulation and RTL synthesis suggest that SC-ConvNets are indeed competitive with conventional binary designs, even without considering inherent error resilience of SC.

Mehta, Brijesh B., Gupta, Ruchika, Rao, Udai Pratap, Muthiyan, Mukesh.  2019.  A Scalable (\$\textbackslashtextbackslashalpha, k\$)-Anonymization Approach using MapReduce for Privacy Preserving Big Data Publishing. 2019 10th International Conference on Computing, Communication and Networking Technologies (ICCCNT). :1—6.
Different tools and sources are used to collect big data, which may create privacy issues. k-anonymity, l-diversity, t-closeness etc. privacy preserving data publishing approaches are used data de-identification, but as multiple sources is used to collect the data, chance of re-identification is very high. Anonymization large data is not a trivial task, hence, privacy preserving approaches scalability has become a challenging research area. Researchers explore it by proposing algorithms for scalable anonymization. We further found that in some scenarios efficient anonymization is not enough, timely anonymization is also required. Hence, to incorporate the velocity of data with Scalable k-Anonymization (SKA) approach, we propose a novel approach, Scalable ( α, k)-Anonymization (SAKA). Our proposed approach outperforms in terms of information loss and running time as compared to existing approaches. With best of our knowledge, this is the first proposed scalable anonymization approach for the velocity of data.
Jouini, Mouna, Ben Arfa Rabai, Latifa.  2016.  A Scalable Threats Classification Model in Information Systems. Proceedings of the 9th International Conference on Security of Information and Networks. :141–144.

Threat classification is extremely important for individuals and organizations, as it is an important step towards realization of information security. In fact, with the progress of information technologies (IT) security becomes a major challenge for organizations which are vulnerable to many types of insiders and outsiders security threats. The paper deals with threats classification models in order to help managers to define threat characteristics and then protect their assets from them. Existing threats classification models are non complete and present non orthogonal threats classes. The aim of this paper is to suggest a scalable and complete approach that classifies security threat in orthogonal way.

Tahat, Amer, Joshi, Sarang, Goswami, Pronnoy, Ravindran, Binoy.  2019.  Scalable Translation Validation of Unverified Legacy OS Code. 2019 Formal Methods in Computer Aided Design (FMCAD). :1–9.

Formally verifying functional and security properties of a large-scale production operating system is highly desirable. However, it is challenging as such OSes are often written in multiple source languages that have no formal semantics - a prerequisite for formal reasoning. To avoid expensive formalization of the semantics of multiple high-level source languages, we present a lightweight and rigorous verification toolchain that verifies OS code at the binary level, targeting ARM machines. To reason about ARM instructions, we first translate the ARM Specification Language that describes the semantics of the ARMv8 ISA into the PVS7 theorem prover and verify the translation. We leverage the radare2 reverse engineering tool to decode ARM binaries into PVS7 and verify the translation. Our translation verification methodology is a lightweight formal validation technique that generates large-scale instruction emulation test lemmas whose proof obligations are automatically discharged. To demonstrate our verification methodology, we apply the technique on two OSes: Google's Zircon and a subset of Linux. We extract a set of 370 functions from these OSes, translate them into PVS7, and verify the correctness of the translation by automatically discharging hundreds of thousands of proof obligations and tests. This took 27.5 person-months to develop.

Chen, G., Wang, D., Li, T., Zhang, C., Gu, M., Sun, J..  2018.  Scalable Verification Framework for C Program. 2018 25th Asia-Pacific Software Engineering Conference (APSEC). :129-138.

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.

Weitz, Konstantin, Woos, Doug, Torlak, Emina, Ernst, Michael D., Krishnamurthy, Arvind, Tatlock, Zachary.  2016.  Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver. Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. :765–780.

Internet Service Providers (ISPs) use the Border Gateway Protocol (BGP) to announce and exchange routes for de- livering packets through the internet. ISPs must carefully configure their BGP routers to ensure traffic is routed reli- ably and securely. Correctly configuring BGP routers has proven challenging in practice, and misconfiguration has led to worldwide outages and traffic hijacks. This paper presents Bagpipe, a system that enables ISPs to declaratively express BGP policies and that automatically verifies that router configurations implement such policies. The novel initial network reduction soundly reduces policy verification to a search for counterexamples in a finite space. An SMT-based symbolic execution engine performs this search efficiently. Bagpipe reduces the size of its search space using predicate abstraction and parallelizes its search using symbolic variable hoisting. Bagpipe's policy specification language is expressive: we expressed policies inferred from real AS configurations, policies from the literature, and policies for 10 Juniper TechLibrary configuration scenarios. Bagpipe is efficient: we ran it on three ASes with a total of over 240,000 lines of Cisco and Juniper BGP configuration. Bagpipe is effective: it revealed 19 policy violations without issuing any false positives.