Protecting the confidentiality of information manipulated by a computing system is one of the most important challenges facing today's cybersecurity community. A promising step toward conquering this challenge is ...
详细信息
ISBN:
(纸本)9781450342612
Protecting the confidentiality of information manipulated by a computing system is one of the most important challenges facing today's cybersecurity community. A promising step toward conquering this challenge is to formally verify that the end-to-end behavior of the computing system really satisfies various information-flow policies. Unfortunately, because today's system software still consists of both C and assembly programs, the end-to-end verification necessarily requires that we not only prove the security properties of individual components, but also carefully preserve these properties through compilation and cross-language linking. In this paper, we present a novel methodology for formally verifying end-to-end security of a software system that consists of both C and assembly programs. We introduce a general definition of observation function that unifies the concepts of policy specification, state indistinguishability, and whole-execution behaviors. We show how to use different observation functions for different levels of abstraction, and how to link different security proofs across abstraction levels using a special kind of simulation that is guaranteed to preserve state indistinguishability. To demonstrate the effectiveness of our new methodology, we have successfully constructed an end-to-end security proof, fully formalized in the Coq proof assistant, of a nontrivial operating system kernel (running on an extended CompCert x86 assembly machine model). Some parts of the kernel are written in C and some are written in assembly;we verify all of the code, regardless of language.
Hop. js is a multitier programming environment for JavaScript. It allows a single JavaScript program to describe the client-side and the server-side components of a web application. Its runtime environment ensures con...
详细信息
ISBN:
(纸本)9781450342193
Hop. js is a multitier programming environment for JavaScript. It allows a single JavaScript program to describe the client-side and the server-side components of a web application. Its runtime environment ensures consistent executions of the application on the server and on the client. This paper overviews the Hop. js design. It shows the JavaScript extensions that makes it possible to conceive web applications globally. It presents how Hop. js interacts with the outside world. It also briefly presents the Hop. js implementation. It presents the Hop. js web server implementation, the handling of server-side parallelism, and the JavaScript and HTML compilers.
This paper introduces Input Responsive Approximation ( IRA), an approach that uses a canary input - a small program input carefully constructed to capture the intrinsic properties of the original input - to automatica...
详细信息
ISBN:
(纸本)9781450342612
This paper introduces Input Responsive Approximation ( IRA), an approach that uses a canary input - a small program input carefully constructed to capture the intrinsic properties of the original input - to automatically control how program approximation is applied on an input-by-input basis. Motivating this approach is the observation that many of the prior techniques focusing on choosing how to approximate arrive at conservative decisions by discounting substantial differences between inputs when applying approximation. The main challenges in overcoming this limitation lie in making the choice of how to approximate both effectively (e.g., the fastest approximation that meets a particular accuracy target) and rapidly for every input. With IRA, each time the approximate program is run, a canary input is constructed and used dynamically to quickly test a spectrum of approximation alternatives. Based on these runtime tests, the approximation that best fits the desired accuracy constraints is selected and applied to the full input to produce an approximate result. We use IRA to select and parameterize mixes of four approximation techniques from the literature for a range of 13 image processing, machine learning, and data mining applications. Our results demonstrate that IRA significantly outperforms prior approaches, delivering an average of 10.2x speedup over exact execution while minimizing accuracy losses in program outputs.
Layout for web documents is a complex process described by the lengthy prose Cascading Style Sheets (CSS) specification. It is difficult to ensure that implementations match this specification. We show how an implemen...
详细信息
ISBN:
(纸本)9781450344371
Layout for web documents is a complex process described by the lengthy prose Cascading Style Sheets (CSS) specification. It is difficult to ensure that implementations match this specification. We show how an implementation can more closely match the specification by using attribute grammars to define layout computations. Particularly, we show how high-level patterns encode the terminology of the specification, discriminating between elements using the same language as in the specification. We also present a new method of injecting artificial structure into an existing tree using reference attribute grammars. The result is a high-level executable specification for CSS layout that can form the basis for a full declarative implementation.
In order to achieve the highest possible performance, the ray traversal and intersection routines at the core of every high-performance ray tracer are usually hand-coded, heavily optimized, and implemented separately ...
详细信息
An operating system (OS) kernel forms the lowest level of any system software stack. The correctness of the OS kernel is the basis for the correctness of the entire system. Recent efforts have demonstrated the feasibi...
详细信息
ISBN:
(纸本)9781450342612
An operating system (OS) kernel forms the lowest level of any system software stack. The correctness of the OS kernel is the basis for the correctness of the entire system. Recent efforts have demonstrated the feasibility of building formally verified general-purpose kernels, but it is unclear how to extend their work to verify the functional correctness of device drivers, due to the non-local effects of interrupts. In this paper, we present a novel compositional framework for building certified interruptible OS kernels with device drivers. We provide a general device model that can be instantiated with various hardware devices, and a realistic formal model of interrupts, which can be used to reason about interruptible code. We have realized this framework in the Coq proof assistant. To demonstrate the effectiveness of our new approach, we have successfully extended an existing verified non-interruptible kernel with our framework and turned it into an interruptible kernel with verified device drivers. To the best of our knowledge, this is the first verified interruptible operating system with device drivers.
Dunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programminglanguage features. While his calculus is type-safe, it is not coherent: different d...
详细信息
ISBN:
(纸本)9781450342193
Dunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programminglanguage features. While his calculus is type-safe, it is not coherent: different derivations for the same expression can elaborate to expressions that evaluate to different values. The lack of coherence is an important disadvantage for adoption of his core calculus in implementations of programminglanguages, as the semantics of the programminglanguage becomes implementation-dependent. This paper presents lambda(i) : a coherent and type-safe calculus with a form of intersection types and a merge operator. Coherence is achieved by ensuring that intersection types are disjoint and programs are sufficiently annotated to avoid type ambiguity. We propose a definition of disjointness where two types A and B are disjoint only if certain set of types are common supertypes of A and B. We investigate three different variants of lambda(i), with three variants of disjointness. In the simplest variant, which does not allow inverted perpendicular types, two types are disjoint if they do not share any common supertypes at all. The other two variants introduce inverted perpendicular types and refine the notion of disjointness to allow two types to be disjoint when the only the set of common supertypes are top-like. The difference between the two variants with inverted perpendicular types is on the definition of top-like types, which has an impact on which types are allowed on intersections. We present a type system that prevents intersection types that are not disjoint, as well as an algorithmic specifications to determine whether two types are disjoint for all three variants.
language workbenches are widely used to implement domain specific languages (DSLs) and their accompanying integrated development environments (IDEs). They help to define the abstract syntax, concrete syntax(es), type ...
详细信息
ISBN:
(纸本)9781450344371
language workbenches are widely used to implement domain specific languages (DSLs) and their accompanying integrated development environments (IDEs). They help to define the abstract syntax, concrete syntax(es), type system, and transformations for the languages. However, there are other language aspects, specifically program analyses and optimizations, that are also crucial to a languageimplementation, but state-of-the-art language workbenches has only limited support for them. The high implementation effort for these language aspects is justifiable for a general-purpose language (GPL), but is not justifiable for DSLs because of their different development economies. To this end, I conduct research on dedicated support for analyses and optimizations for DSLs in language workbenches. My main goal is to develop declarative meta languages that help to define static program analyses and that capture and automate patterns and techniques of optimizations. The research directions are directly driven by industrial need, and upon successful completion, the results would be applied in projects centered around DSLs for high-performance computing (HPC), insurance, and concurrent embedded systems.
JavaScript is the de facto language of the Web, but is notoriously error-prone to use. 65% of common bugs like undefined/null variable usage are DOM-related. Besides DOM, JS APIs are also expected to manipulate graphi...
详细信息
ISBN:
(纸本)9781450344371
JavaScript is the de facto language of the Web, but is notoriously error-prone to use. 65% of common bugs like undefined/null variable usage are DOM-related. Besides DOM, JS APIs are also expected to manipulate graphic hardware and asynchronous I/O, which makes the condition even worse. Although WebIDL provides a formal contract between JS developers and platform implementation, its expressivity is too limited to support deep checking of API misuses. We propose the eXtended WebIDL (xWIDL) language and a modular API misuses checking framework based on xWIDL. We discuss how to handle the data exchange between JS analyzer and SMT-based verifier. Finally, we test our implementation in a case study manner and report our findings on its efficiency and modularity.
Coding conventions are lexical, syntactic or semantic restrictions enforced on top of a software language for the sake of consistency within the source base. Specifying coding conventions is currently an open problem ...
详细信息
ISBN:
(纸本)9781450344470
Coding conventions are lexical, syntactic or semantic restrictions enforced on top of a software language for the sake of consistency within the source base. Specifying coding conventions is currently an open problem in software language engineering, addressed in practice by resorting to natural language descriptions which complicate conformance verification. In this paper we present an endeavour to solve this problem for the case of CSS - a ubiquitous software language used for specifying appearance of hypertextual content separately from the content itself. The paper contains the results of domain analysis, a short report on an empirically obtained catalogue of 143 unique CSS coding conventions, the domain-specific ontology for the domain of detecting violations, the design of CssCoco, a language for expressing coding conventions of CSS, as well as a description of the tool we developed to detect violations of conventions specified in this DSL.
暂无评论