Biblio
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 is a full paper for innovate practice. Building a private cloud or using a public cloud is now feasible at many institutions. This paper presents the innovative design of cloudbased labs and programming assignments for a networking course and a cybersecurity course, and our experiences of innovatively using the private cloud at our institution to support these learning activities. It is shown by the instructor's observations and student survey data that our approach benefits learning and teaching. This approach makes it possible and secure to develop some learning activities that otherwise would not be allowed on physical servers. It enables the instructor to support students' desire of developing programs in their preferred programming languages. It allows students to debug and test their programs on the same platform to be used by the instructor for testing and grading. The instructor does not need to spend extra time administrating the computing environments. A majority (88% or more) of the students agree that working on those learning activities in the private cloud not only helps them achieve the course learning objectives, but also prepares them for their future careers.
A new program has been developed for style and authorship attribution. Differentiation of styles by transcription symbols has proved to be efficient The novel approach involves a combination of two ways of transforming texts into their transcription variants. The java programming language makes it possible to improve efficiency of style and authorship attribution.
Scala programming language combines object-oriented and functional programming in one concise, high-level language, and the language supports static types that help to avoid bugs in complex programs. This paper proposes a dynamic taint analyzer called ScalaTaint for Scala applications. The analyzer traces the propagation of malicious inputs from untrusted sources to sensitive sink methods in programs that can be exploited by adversaries. In this work, we evaluated the accuracy of ScalaTaint with a security benchmark suite including 7 projects in Scala. As a result, our analyzer could report 49 vulnerabilities within 753,372 lines of code. Moreover, the result of our performance measurement on ScalaBench shows 67% runtime overhead that demonstrates the usefulness and efficiently of our technique in comparison with similar tools.
This paper presents Checked C, an extension to C designed to support spatial safety, implemented in Clang and LLVM. Checked C's design is distinguished by its focus on backward-compatibility, incremental conversion, developer control, and enabling highly performant code. Like past approaches to a safer C, Checked C employs a form of checked pointer whose accesses can be statically or dynamically verified. Performance evaluation on a set of standard benchmark programs shows overheads to be relatively low. More interestingly, Checked C introduces the notions of a checked region and bounds-safe interfaces.
Today, maintaining the security of the web application is of great importance. Sites Intermediate Script (XSS) is a security flaw that can affect web applications. This error allows an attacker to add their own malicious code to HTML pages that are displayed to the user. Upon execution of the malicious code, the behavior of the system or website can be completely changed. The XSS security vulnerability is used by attackers to steal the resources of a web browser such as cookies, identity information, etc. by adding malicious Java Script code to the victim's web applications. Attackers can use this feature to force a malicious code worker into a Web browser of a user, since Web browsers support the execution of embedded commands on web pages to enable dynamic web pages. This work has been proposed as a technique to detect and prevent manipulation that may occur in web sites, and thus to prevent the attack of Site Intermediate Script (XSS) attacks. Ayrica has developed four different languages that detect XSS explanations with Asp.NET, PHP, PHP and Ruby languages, and the differences in the detection of XSS attacks in environments provided by different programming languages.
Complex safety-critical devices require dependable communication. Dependability includes confidentiality and integrity as much as safety. Encrypting gateways with demilitarized zones, Multiple Independent Levels of Security architectures and the infamous Air Gap are diverse integration patterns for safety-critical infrastructure. Though resource restricted embedded safety devices still lack simple, certifiable, and efficient cryptography implementations. Following the recommended formal methods approach for safety-critical devices, we have implemented proven cryptography algorithms in the qualified model based language Scade as the Safety Leveraged Implementation of Data Encryption (SLIDE) library. Optimization for the synchronous dataflow language is discussed in the paper. The implementation for public-key based encryption and authentication is evaluated for real-world performance. The feasibility is shown by execution time benchmarks on an industrial safety microcontroller platform running a train control safety application.
Programming languages have long incorporated type safety, increasing their level of abstraction and thus aiding programmers. Type safety eliminates whole classes of security-sensitive bugs, replacing the tedious and error-prone search for such bugs in each application with verifying the correctness of the type system. Despite their benefits, these protections often end at the process boundary, that is, type safety holds within a program but usually not to the file system or communication with other programs. Existing operating system approaches to bridge this gap require the use of a single programming language or common language runtime. We describe the deep integration of type safety in Ethos, a clean-slate operating system which requires that all program input and output satisfy a recognizer before applications are permitted to further process it. Ethos types are multilingual and runtime-agnostic, and each has an automatically generated unique type identifier. Ethos bridges the type-safety gap between programs by (1) providing a convenient mechanism for specifying the types each program may produce or consume, (2) ensuring that each type has a single, distributed-system-wide recognizer implementation, and (3) inescapably enforcing these type constraints.
The innovations in communication and computing technologies are changing the way we carry-out the tasks in our daily lives. These revolutionary and disrupting technologies are available to the users in various hardware form-factors like Smart Phones, Embedded Appliances, Configurable or Customizable add-on devices, etc. One such technology is Bluetooth [1], which enables the users to communicate and exchange various kinds of information like messages, audio, streaming music and file transfer in a Personal Area Network (PAN). Though it enables the user to carry-out these kinds of tasks without much effort and infrastructure requirements, they inherently bring with them the security and privacy concerns, which need to be addressed at different levels. In this paper, we present an application-layer framework, which provides strong mutual authentication of applications, data confidentiality and data integrity independent of underlying operating system. It can make use of the services of different Cryptographic Service Providers (CSP) on different operating systems and in different programming languages. This framework has been successfully implemented and tested on Android Operating System on one end (using Java language) and MS-Windows 7 Operating System on the other end (using ANSI C language), to prove the framework's reliability/compatibility across OS, Programming Language and CSP. This framework also satisfies the three essential requirements of Security, i.e. Confidentiality, Integrity and Availability, as per the NIST Guide to Bluetooth Security specification and enables the developers to suitably adapt it for different kinds of applications based on Bluetooth Technology.
An authenticated data structure (ADS) is a data structure whose operations can be carried out by an untrusted prover, the results of which a verifier can efficiently check as authentic. This is done by having the prover produce a compact proof that the verifier can check along with each operation's result. ADSs thus support outsourcing data maintenance and processing tasks to untrusted servers without loss of integrity. Past work on ADSs has focused on particular data structures (or limited classes of data structures), one at a time, often with support only for particular operations.
This paper presents a generic method, using a simple extension to a ML-like functional programming language we call λ• (lambda-auth), with which one can program authenticated operations over any data structure defined by standard type constructors, including recursive types, sums, and products. The programmer writes the data structure largely as usual and it is compiled to code to be run by the prover and verifier. Using a formalization of λ• we prove that all well-typed λ• programs result in code that is secure under the standard cryptographic assumption of collision-resistant hash functions. We have implemented λ• as an extension to the OCaml compiler, and have used it to produce authenticated versions of many interesting data structures including binary search trees, red-black+ trees, skip lists, and more. Performance experiments show that our approach is efficient, giving up little compared to the hand-optimized data structures developed previously.