Continuous Verification of Network Security Compliance

Continuous verification of network security compliance is an accepted need. Especially, the analysis of stateful packet filters plays a central role for network security in practice. But the few existing tools which support the analysis of stateful packet filters are based on general applicable formal methods like Satifiability Modulo Theories (SMT) or theorem prover and show runtimes in the order of minutes to hours making them unsuitable for continuous compliance verification.<br>In this work, we address these challenges and present the concept of state shell interweaving to transform a stateful firewall rule set into a stateless rule set. This allows us to reuse any fast domain specific engine from the field of data plane verification tools leveraging smart, very fast, and domain specialized data structures and algorithms including Header Space Analysis (HSA). First, we introduce the formal language FPL that enables a high-level human-understandable specification of the desired state of network security. Second, we demonstrate the instantiation of a compliance process using a verification framework that analyzes the configuration of complex networks and devices - including stateful firewalls - for compliance with FPL policies. Our evaluation results show the scalability of the presented approach for the well known Internet2 and Stanford benchmarks as well as for large firewall rule sets where it outscales state-of-the-art tools by a factor of over 41.

Verification of MILS Partition Scheduling Module Using Layered Methods

MILS partition scheduling module ensures isolation of data between different domains completely by enforcing secure strategies. Although small in size, it involves complicated data structures and algorithms that make monolithic verification of the scheduling module difficult using traditional verification logic (e.g., separation logic). In this paper, we simplify the verification task by dividing data representation and data operation into different layers and then to link them together by composing a series of abstraction layers. The layered method also supports function calls from higher implementation layers into lower abstraction layers, allowing us to ignore implementation details in the lower implementation layers. Using this methodology, we have verified a realistic MILS partition scheduling module that can schedule operating systems (Ubuntu 14.04, VxWorks 6.8 and RTEMS 11.0) located in different domains. The entire verification has been mechanized in the Coq Proof Assistant.

A Fresh Look at Zones and Octagons

Zones and Octagons are popular abstract domains for static program analysis. They enable the automated discovery of simple numerical relations that hold between pairs of program variables. Both domains are well understood mathematically but the detailed implementation of static analyses based on these domains poses many interesting algorithmic challenges. In this article, we study the two abstract domains, their implementation and use. Utilizing improved data structures and algorithms for the manipulation of graphs that represent difference-bound constraints, we present fast implementations of both abstract domains, built around a common infrastructure. We compare the performance of these implementations against alternative approaches offering the same precision. We quantify the differences in performance by measuring their speed and precision on standard benchmarks. We also assess, in the context of software verification, the extent to which the improved precision translates to better verification outcomes. Experiments demonstrate that our new implementations improve the state of the art for both Zones and Octagons significantly.

Research on Multicore Key-Value Storage System for Domain Name Storage

This article proposes a domain name caching method for the multicore network-traffic capture system, which significantly improves insert latency, throughput and hit rate. The caching method is composed of caching replacement algorithm, cache set method. The method is easy to implement, low in deployment cost, and suitable for various multicore caching systems. Moreover, it can reduce the use of locks by changing data structures and algorithms. Experimental results show that compared with other caching system, our proposed method reaches the highest throughput under multiple cores, which indicates that the cache method we proposed is best suited for domain name caching.

Research on the Practical Teaching of Data Structures and Algorithms Course

The success or failure of practical teaching in data structures and algorithms course determines the success or failure of the course group. The reform of practical teaching in this course takes the course group as the background and aims to meet the needs of students at different levels. It proposes a hierarchical practical teaching mode involving three levels in terms of foundation, design, and synthesis driven by cases throughout the whole course group and a fine process control mechanism based on multi-stage process assessment.

Value trace problems with assisting references for Python programming self-study

Purpose This study aims to present the value trace problem (VTP) for Python programming self-study, by extending the works for Java programming learning assistant system. In total, 130 VTP instances are generated using Python codes in textbooks and websites that cover basic/advanced grammar topics, fundamental data structures and algorithms and two common library usages. Besides, assisting references on Python programming topics related to the VTP instances are introduced to assist novice learners in solving them efficiently. Design/methodology/approach PyPLAS offers the VTP to study grammar topics and library usage through code reading. A VTP instance asks a learner to trace the actual values of important variables or output messages in the given source code. The correctness of any answer is checked through string matching. Findings The applications to 48 undergraduate students in Myanmar and Indonesia confirm the validity of the proposal in Python programming self-studies by novice learners. Originality/value The applications to 48 undergraduate students in Myanmar and Indonesia confirm the validity of the proposal in Python programming self-studies by novice learners.

Review of The Foundations of Computability Theory (Second Edition) by Borut Robič

Computability theory forms the foundation for much of theoretical computer science. Many of our great unsolved questions stem from the need to understand what problems can even be solved. The greatest question of computer science, P vs. NP, even sidesteps this entirely, asking instead how efficiently we can find solutions for the problems that we know are solvable. For many students both at the undergraduate and graduate level, a first exposure to computability theory follows a standard sequence on data structures and algorithms and students often marvel at the first results they see on undecidability - how could we possibly prove that we can never solve a problem? This book, in contrast with other books that are often used as first exposures to computability, finite automata, Turing machines, and the like, focuses very specifically on the notion of what is computable and how computability theory, as a science unto itself, fits into the grander scheme. The book is appropriate for advanced undergraduates and beginning graduate students in computer science or mathematics who are interested in theoretical computer science. Robič sidesteps the standard theoretical computer science progression - understanding finite automata and pushdown automata before moving into Turing machines - by setting the stage with Hilbert's program and mathematical prerequisites before introducing the Turing machine absent the usual prerequisites, and then introducing advanced topics often absent in introductory texts. Most chapters are relatively short and contain problem sets, making it appropriate for both a classroom text or for self-study.

Visualization Technologies, Cognition and Learner

COGNITION, refers to the process of thinking, comprehension, judging the problem solving methodologies and various aspects of human mind and intelligence. Human intelligence is, not mere perception but inexplicable roles played by all the five senses. In rationalising the role of all these senses there is another important, rather most important of all sixth sense. The basic role is visualization which is the basis of all the hunches and inspiration within the realm of human being. Now, cognition has various effects on the education of humans. In fact, the visualization technology can be used for helping learners in understanding, implementation and prototyping of various algorithms using different data structure in Computer science and technology. This can be very helpful in real-time implementation in classrooms and in various web applications, including the implementation of various fun 2-D and 3-D characters. These methodologies not only helps in cognitive learning of various data structures and algorithms but also built a rapport for visualization technology and cognitive learning. Thus, visualization technology prototype can be innovation at a psychological level and be helpful in long run.