Biblio

Server-side web applications are vulnerable to request races. While some previous studies of real-world request races exist, they primarily focus on the root cause of these bugs. To better combat request races in server-side web applications, we need a deep understanding of their characteristics. In this paper, we provide a complementary focus on race effects and fixes with an enlarged set of request races from web applications developed with Object-Relational Mapping (ORM) frameworks. We revisit characterization questions used in previous studies on newly included request races, distinguish the external and internal effects of request races, and relate requestrace fixes with concurrency control mechanisms in languages and frameworks for developing server-side web applications. Our study reveals that: (1) request races from ORM-based web applications share the same characteristics as those from raw-SQL web applications; (2) request races violating application semantics without explicit crashes and error messages externally are common, and latent request races, which only corrupt some shared resource internally but require extra requests to expose the misbehavior, are also common; and (3) various fix strategies other than using synchronization mechanisms are used to fix request races. We expect that our results can help developers better understand request races and guide the design and development of tools for combating request races.

Blockchain smart contracts are prevalent nowadays as numerous applications are developed based on this feature. Though smart contracts are important and widely used, they contain certain vulnerabilities. This paper discusses various security issues that arise in smart contract applications. They are categorized in the smart contract platform, the applications that integrate with the Blockchain, and the vulnerabilities in smart contract code. A detailed study of smart contract-specific vulnerabilities and the defense against those vulnerabilities are presented in this article. Because of certain limitations of platforms or programming language used to write smart contract, there are possibilities of attacks on smart contracts. Hence different security measures or precautions to be taken while writing the smart contract code is discussed in this article. This will prevent the potential attacks happening on Blockchain distributed applications.

Peer review is a widely utilized pedagogical feedback mechanism for engaging students, which has been shown to improve educational outcomes. However, we find limited discussion and empirical measurement of peer review in visualization coursework. In addition to engagement, peer review provides direct and diverse feedback and reinforces recently-learned course concepts through critical evaluation of others’ work. In this paper, we discuss the construction and application of peer review in a computer science visualization course, including: projects that reuse code and visualizations in a feedback-guided, continual improvement process and a peer review rubric to reinforce key course concepts. To measure the effectiveness of the approach, we evaluate student projects, peer review text, and a post-course questionnaire from 3 semesters of mixed undergraduate and graduate courses. The results indicate that course concepts are reinforced with peer review—82% reported learning more because of peer review, and 75% of students recommended continuing it. Finally, we provide a road-map for adapting peer review to other visualization courses to produce more highly engaged students.

The use of software daily has become inevitable nowadays. Almost all everyday tools and the most different areas (e.g., medicine or telecommunications) are dependent on software. The C programming language is one of the most used languages for software development, such as operating systems, drivers, embedded systems, and industrial products. Even with the appearance of new languages, it remains one of the most used [1] . At the same time, C lacks verification mechanisms, like array boundaries, leaving the entire responsibility to the developer for the correct management of memory and resources. These weaknesses are at the root of buffer overflows (BO) vulnerabilities, which range the first place in the CWE’s top 25 of the most dangerous weaknesses [2] . The exploitation of BO when existing in critical safety systems, such as railways and autonomous cars, can have catastrophic effects for manufacturers or endanger human lives.

Static analyzers have become increasingly popular both as developer tools and as subjects of empirical studies. Whereas static analysis tools exist for disparate programming languages, the bulk of the empirical research has focused on the popular Java programming language. In this paper, we investigate to what extent some known results about using static analyzers for Java change when considering C\#-another popular object-oriented language. To this end, we combine two replications of previous Java studies. First, we study which static analysis tools are most widely used among C\# developers, and which warnings are more commonly reported by these tools on open-source C\# projects. Second, we develop and empirically evaluate EagleRepair: a technique to automatically fix code in response to static analysis warnings; this is a replication of our previous work for Java [20]. Our replication indicates, among other things, that 1) static code analysis is fairly popular among C\# developers too; 2) Re-Sharper is the most widely used static analyzer for C\#; 3) several static analysis rules are commonly violated in both Java and C\# projects; 4) automatically generating fixes to static code analysis warnings with good precision is feasible in C\#. The EagleRepair tool developed for this research is available as open source.

Non-interference is a program property that ensures the absence of information leaks. In the context of programming languages, there exist two common approaches for establishing non-interference: type systems and program logics. Type systems provide strong automation (by means of type checking), but they are inherently restrictive in the kind of programs they support. Program logics support challenging programs, but they typically require significant human assistance, and cannot handle modules or higher-order programs.To connect these two approaches, we present SeLoC—a separation logic for non-interference, on top of which we build a type system using the technique of logical relations. By building a type system on top of separation logic, we can compositionally verify programs that consist of typed and untyped parts. The former parts are verified through type checking, while the latter parts are verified through manual proof.The core technical contribution of SeLoC is a relational form of weakest preconditions that can track information flow using separation logic resources. SeLoC is fully machine-checked, and built on top of the Iris framework for concurrent separation logic in Coq. The integration with Iris provides seamless support for fine-grained concurrency, which was beyond the reach of prior type systems and program logics for non-interference.

A kitchen underpinned by the Internet of Things (IoT) requires the management of complex procedural processes. This is due to the fact that when supporting an end-user in the preparation of even only one dish, various devices may need to coordinate with each other. Additionally, it is challenging— yet desirable—to enable an end-user to program their kitchen devices according to their preferred behaviour and to allow them to visualise and track their cooking workflows. In this paper, we compared two semantic representations, namely, Behaviour Trees and the DX-MAN model. We analysed these representations based on their suitability for a range of end-users (i.e., novice to experienced). The methodology required the analysis of smart kitchen user requirements, from which we inferred that the main architectural requirements for IoT cooking workflows are variability and compositionality. Guided by the user requirements, we examined various scenarios and analysed workflow complexity and feasibility for each representation. On the one hand, we found that execution complexity tends to be higher on Behaviour Trees. However, due to their fallback node, they provide more transparency on how to recover from unprecedented circumstances. On the other hand, parameter complexity tends to be somewhat higher for the DX-MAN model. Nevertheless, the DX-MAN model can be favourable due to its compositionality aspect and the ease of visualisation it can offer.

Kotlin is a relatively new programming language from JetBrains: its development started in 2010 with release 1.0 done in early 2016. The Kotlin compiler, while slowly and steadily becoming more and more mature, still crashes from time to time on the more tricky input programs, not least because of the complexity of its features and their interactions. This makes it a great target for fuzzing, even the basic forms of which can find a significant number of Kotlin compiler crashes. There is a problem with fuzzing, however, closely related to the cause of the crashes: generating a random, non-trivial and semantically valid Kotlin program is hard. In this paper, we talk about type-centriccompilerfuzzing in the form of type-centricenumeration, an approach inspired by skeletal program enumeration [1] and based on a combination of generative and mutation-based fuzzing, which solves this problem by focusing on program types. After creating the skeleton program, we fill the typed holes with fragments of suitable type, created via generation and enhanced by semantic-aware mutation. We implemented this approach in our Kotlin compiler fuzzing framework called Backend Bug Finder (BBF) and did an extensive evaluation, not only testing the real-world feasibility of our approach, but also comparing it to other compiler fuzzing techniques. The results show our approach to be significantly better compared to other fuzzing approaches at generating semantically valid Kotlin programs, while creating more interesting crash-inducing inputs at the same time. We managed to find more than 50 previously unknown compiler crashes, of which 18 were considered important after their triage by the compiler team.

Network Centric Warfare (NCW) is a design that supports information excellence for the concept of military operations. Network Centric Warfare is currently being developed as the basis for the operating concept, namely multidimensional operations. TNI operations do not rely on conventional warfare. TNI operations must work closely with the TNI Puspen team, territorial intelligence, TNI cyber team, and support task force. Sending digital images sent online requires better techniques to maintain confidentiality. The purpose of this research is to design digital image security with AES cryptography and discrete wavelet transform method on interoperability and to utilize and study discrete wavelet transform method and AES algorithm on interoperability for digital image security. The AES cryptography technique in this study is used to protect and maintain the confidentiality of the message while the Discrete Wavelet Transform in this study is used to reduce noise by applying a discrete wavelet transform, which consists of three main steps, namely: image decomposition, thresholding process and image reconstruction. The result of this research is that Digital Image Security to support TNI interoperability has been produced using the C \# programming language framework. NET and Xampp to support application development. Users can send data in the form of images. Discrete Wavelet Transformation in this study is used to find the lowest value against the threshold so that the resulting level of security is high. Testing using the AESS algorithm to encrypt and decrypt image files using key size and block size.

The Linux kernel is implemented in C, an unsafe programming language, which puts the burden of memory management, type and bounds checking, and error handling in the hands of the developer. Hundreds of buffer overflow bugs have compromised Linux systems over the years, leading to endless layers of mitigations applied on top of C. In contrast, the D programming language offers automated memory safety checks and modern features such as OOP, templates and functional style constructs. In addition, interoper-ability with C is supported out of the box. However, to integrate a D module with the Linux kernel it is required that the needed C header files are translated to D header files. This is a tedious, time consuming, manual task. Although a tool to automate this process exists, called DPP, it does not work with the complicated, sometimes convoluted, kernel code. In this paper, we improve DPP with the ability to translate any Linux kernel C header to D. Our work enables the development and integration of D code inside the Linux kernel, thus facilitating a method of making the kernel memory safe.

It is well-known, and often a topic of heated debates, that programs in some programming languages are more concise than in others. This is a relevant factor when comparing or aggregating volume-impacted metrics on source code written in a combination of programming languages. In this paper, we present a model for measuring the conciseness of programming languages in a consistent, objective and evidence-based way. We present the approach, explain how it is founded on information theoretical principles, present detailed analysis steps and show the quantitative results of applying this model to a large benchmark of diverse commercial software applications. We demonstrate that our metric for language conciseness is strongly correlated with both an alternative analytical approach, and with a large scale developer survey, and show how its results can be applied to improve software metrics for multi-language applications.

Epistemic logic can specify many design requirements of privacy and security of multi-agent systems (MAS). The existing model checkers of epistemic logic use some programming languages to describe MAS, induce Kripke models as the behavioral representation of MAS, apply Ordered Binary Decision Diagrams (OBDD) to encode Kripke models to solve their state explosion problem and verify epistemic logic based on the encoded Kripke models. However, these programming languages are usually non-intuitive. More seriously, their OBDD-based model checking processes are often time-consuming due to their dynamic variable ordering for OBDD. Therefore, we define Knowledge-oriented Petri Nets (KPN) to intuitively describe MAS, induce similar reachability graphs as the behavioral representation of KPN, apply OBDD to encode all reachable states, and finally verify epistemic logic. Although we also use OBDD, we adopt a heuristic method for the computation of a static variable order instead of dynamic variable ordering. More importantly, while verifying an epistemic formula, we dynamically generate its needed similar relations, which makes our model checking process much more efficient. In this paper, we introduce our work.

Language-based information flow control (IFC) aims to provide guarantees about information propagation in computer systems having multiple security levels. Existing IFC systems extend the lattice model of Denning's, enforcing transitive security policies by tracking information flows along with a partially ordered set of security levels. They yield a transitive noninterference property of either confidentiality or integrity. In this paper, we explore IFC for security policies that are not necessarily transitive. Such nontransitive security policies avoid unwanted or unexpected information flows implied by transitive policies and naturally accommodate high-level coarse-grained security requirements in modern component-based software. We present a novel security type system for enforcing nontransitive security policies. Unlike traditional security type systems that verify information propagation by subtyping security levels of a transitive policy, our type system relaxes strong transitivity by inferring information flow history through security levels and ensuring that they respect the nontransitive policy in effect. Such a type system yields a new nontransitive noninterference property that offers more flexible information flow relations induced by security policies that do not have to be transitive, therefore generalizing the conventional transitive noninterference. This enables us to directly reason about the extent of information flows in the program and restrict interactions between security-sensitive and untrusted components.

A common technique for building ICT systems is to build them as successive layers of bstraction: for instance, the Instruction Set Architecture (ISA) is an abstraction of the hardware, and compilers or interpreters build higher level abstractions on top of the ISA.The functionality of an ICT application can often be understood by considering only a single level of abstraction. For instance the source code of the application defines the functionality using the level of abstraction of the source programming language. Functionality can be well understood by just studying this source code.Many important security issues in ICT system however are cross-layer issues: they can not be understood by considering the system at a single level of abstraction, but they require understanding how multiple levels of abstraction are implemented. Attacks may rely on, or exploit, implementation details of one or more layers below the source code level of abstraction.The purpose of this paper is to illustrate this cross-layer nature of security by discussing old and new examples of cross-layer security issues, and by providing a classification of these issues.

Information Flow Control (IFC) is a collection of techniques for ensuring a no-write-down no-read-up style security policy known as noninterference. Traditional methods for both static (e.g. type systems) and dynamic (e.g. runtime monitors) IFC suffer from untenable numbers of false alarms on real-world programs. Secure Multi-Execution (SME) promises to provide secure information flow control without modifying the behaviour of already secure programs, a property commonly referred to as transparency. Implementations of SME exist for the web in the form of the FlowFox browser and as plug-ins to several programming languages. Furthermore, SME can in theory work in a black-box manner, meaning that it can be programming language agnostic, making it perfect for securing legacy or third-party systems. As such SME, and its variants like Multiple Facets (MF) and Faceted Secure Multi-Execution (FSME), appear to be a family of panaceas for the security engineer. The question is, how come, given all these advantages, that these techniques are not ubiquitous in practice? The answer lies, partially, in the issue of runtime and memory overhead. SME and its variants are prohibitively expensive to deploy in many non-trivial situations. The natural question is why is this the case? On the surface, the reason is simple. The techniques in the SME family all rely on the idea of multi-execution, running all or parts of a program multiple times to achieve noninterference. Naturally, this causes some overhead. However, the predominant thinking in the IFC community has been that these overheads can be overcome. In this paper we argue that there are fundamental reasons to expect this not to be the case and prove two key theorems: (1) All transparent enforcement is polynomial time equivalent to multi-execution. (2) All black-box enforcement takes time exponential in the number of principals in the security lattice. Our methods also allow us to answer, in the affirmative, an open question about the possibility of secure and transparent enforcement of a security condition known as Termination Insensitive Noninterference.

This article shows the analogy between natural language texts and quantum-like systems on the example of the Bell test calculating. The applicability of the well-known Bell test for texts in Russian is investigated. The possibility of using this test for the text separation on the topics corresponding to the user query in information retrieval system is shown.

Much recent work focuses on finding bugs and security vulnerabilities in smart contracts written in existing languages. Although this approach may be helpful, it does not address flaws in the underlying programming language, which can facilitate writing buggy code in the first place. We advocate a re-thinking of the blockchain software engineering tool set, starting with the programming language in which smart contracts are written. In this paper, we propose and justify requirements for a new generation of blockchain software development tools. New tools should (1) consider users' needs as a primary concern; (2) seek to facilitate safe development by detecting relevant classes of serious bugs at compile time; (3) as much as possible, be blockchain-agnostic, given the wide variety of different blockchain platforms available, and leverage the properties that are common among blockchain environments to improve safety and developer effectiveness.

For a long time, the most important approach for detecting malicious applications was the use of static, hash-based signatures. This approach provides a fast response time, has a low performance overhead and is very stable due to its simplicity. However, with the rapid growth in the number of malware, as well as their increased complexity in terms of polymorphism and evasion, the era of reactive security solutions started to fade in favor of new, proactive approaches such as behavior based detection. We propose a novel approach that uses an interpreter virtual machine to run proactive behavior heuristics from bytecode signatures, thus combining the advantages of behavior based detection with those of signatures. Based on our approximation, using this approach we succeeded to reduce by 85% the time required to update a behavior based detection solution to detect new threats, while continuing to benefit from the versatility of behavior heuristics.

In this paper we propose a solution to support iOS developers in creating better applications, to use static analysis to investigate source code and detect secure coding issues while simultaneously pointing out good practices and/or secure APIs they should use.

Good programming languages provide helpful abstractions for writing secure code, but the security properties of the source language are generally not preserved when compiling a program and linking it with adversarial code in a low-level target language (e.g., a library or a legacy application). Linked target code that is compromised or malicious may, for instance, read and write the compiled program's data and code, jump to arbitrary memory locations, or smash the stack, blatantly violating any source-level abstraction. By contrast, a fully abstract compilation chain protects source-level abstractions all the way down, ensuring that linked adversarial target code cannot observe more about the compiled program than what some linked source code could about the source program. However, while research in this area has so far focused on preserving observational equivalence, as needed for achieving full abstraction, there is a much larger space of security properties one can choose to preserve against linked adversarial code. And the precise class of security properties one chooses crucially impacts not only the supported security goals and the strength of the attacker model, but also the kind of protections a secure compilation chain has to introduce. We are the first to thoroughly explore a large space of formal secure compilation criteria based on robust property preservation, i.e., the preservation of properties satisfied against arbitrary adversarial contexts. We study robustly preserving various classes of trace properties such as safety, of hyperproperties such as noninterference, and of relational hyperproperties such as trace equivalence. This leads to many new secure compilation criteria, some of which are easier to practically achieve and prove than full abstraction, and some of which provide strictly stronger security guarantees. For each of the studied criteria we propose an equivalent “property-free” characterization that clarifies which proof techniques apply. For relational properties and hyperproperties, which relate the behaviors of multiple programs, our formal definitions of the property classes themselves are novel. We order our criteria by their relative strength and show several collapses and separation results. Finally, we adapt existing proof techniques to show that even the strongest of our secure compilation criteria, the robust preservation of all relational hyperproperties, is achievable for a simple translation from a statically typed to a dynamically typed language.

Formal verification of infinite-state systems, and distributed systems in particular, is a long standing research goal. In the deductive verification approach, the programmer provides inductive invariants and pre/post specifications of procedures, reducing the verification problem to checking validity of logical verification conditions. This check is often performed by automated theorem provers and SMT solvers, substantially increasing productivity in the verification of complex systems. However, the unpredictability of automated provers presents a major hurdle to usability of these tools. This problem is particularly acute in case of provers that handle undecidable logics, for example, first-order logic with quantifiers and theories such as arithmetic. The resulting extreme sensitivity to minor changes has a strong negative impact on the convergence of the overall proof effort.

Software-defined networks provide new facilities for deploying security mechanisms dynamically. In particular, it is possible to build and adjust security chains to protect the infrastructures, by combining different security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. It is important to ensure that these security chains, in view of their complexity and dynamics, are consistent and do not include security violations. We propose in this paper an automated strategy for supporting the verification of security chains in software-defined networks. It relies on an architecture integrating formal verification methods for checking both the control and data planes of these chains, before their deployment. We describe algorithms for translating specifications of security chains into formal models that can then be verified by SMT1 solving or model checking. Our solution is prototyped as a package, named Synaptic, built as an extension of the Frenetic family of SDN programming languages. The performances of our approach are evaluated through extensive experimentations based on the CVC4, veriT, and nuXmv checkers.

Software-defined networks provide new facilities for deploying security mechanisms dynamically. In particular, it is possible to build and adjust security chains to protect the infrastructures, by combining different security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. It is important to ensure that these security chains, in view of their complexity and dynamics, are consistent and do not include security violations. We propose in this paper an automated strategy for supporting the verification of security chains in software-defined networks. It relies on an architecture integrating formal verification methods for checking both the control and data planes of these chains, before their deployment. We describe algorithms for translating specifications of security chains into formal models that can then be verified by SMT1 solving or model checking. Our solution is prototyped as a package, named Synaptic, built as an extension of the Frenetic family of SDN programming languages. The performances of our approach are evaluated through extensive experimentations based on the CVC4, veriT, and nuXmv checkers.

Protecting data confidentiality and integrity has become increasingly important in modern software. Sometimes, access control mechanisms come short and solutions on the application-level are needed. An approach can rely on enforcing information security using some features provided by certain programming languages. Several different solutions addressing this problem have been presented in literature, and entire new languages or libraries have been built from scratch. Some of them use type systems to let the compiler check for vulnerable code. In this way we are able to rule out those implementations which do not meet a certain security requirement. In this paper we use Haskell's type system to enforce three key properties of information security: non-interference and flexible declassification policies, strict input validation, and secure computations on untainted and trusted values. We present a functional lightweight library for applications with data integrity and confidentiality issues. Our contribute relies on a compile time enforcing of the aforementioned properties. Our library is wholly generalized and might be adapted for satisfying almost every security requirement.