Commit a8b71dd0 authored by pmaksimo's avatar pmaksimo
Browse files

gillian

parent 0fdea59f
......@@ -1446,20 +1446,20 @@ the JavaScript variable store.},
year = {2018},
project = { web },
doi = {10.1145/3158138},
abstract = {The dynamic nature of JavaScript and its complex semantics make it a difficult target for logic-based verification.
We introduce JaVerT, a semi-automatic JavaScript Verification Toolchain, based on separation logic and aimed at the specialist developer wanting rich,
mechanically verified specifications of critical JavaScript code. To specify JavaScript programs,
we design abstractions that capture its key heap structures (for example, prototype chains and function closures),
allowing the developer to write clear and succinct specifications with minimal knowledge of the JavaScript internals.
To verify JavaScript programs, we develop JaVerT, a verification pipeline consisting of: JS-2-JSIL,
a well-tested compiler from JavaScript to JSIL, an intermediate goto language capturing the fundamental dynamic features of JavaScript;
JSIL Verify, a semi-automatic verification tool based on a sound JSIL separation logic;
and verified axiomatic specifications of the JavaScript internal functions.
Using JaVerT, we verify functional correctness properties of:
data-structure libraries (key-value map, priority queue) written in an object-oriented style;
operations on data structures such as binary search trees (BSTs) and lists; examples illustrating function closures;
and test cases from the official ECMAScript test suite. The verification times suggest that reasoning about larger,
more complex code using JaVerT is feasible.
abstract = {The dynamic nature of JavaScript and its complex semantics make it a difficult target for logic-based verification.
We introduce JaVerT, a semi-automatic JavaScript Verification Toolchain, based on separation logic and aimed at the specialist developer wanting rich,
mechanically verified specifications of critical JavaScript code. To specify JavaScript programs,
we design abstractions that capture its key heap structures (for example, prototype chains and function closures),
allowing the developer to write clear and succinct specifications with minimal knowledge of the JavaScript internals.
To verify JavaScript programs, we develop JaVerT, a verification pipeline consisting of: JS-2-JSIL,
a well-tested compiler from JavaScript to JSIL, an intermediate goto language capturing the fundamental dynamic features of JavaScript;
JSIL Verify, a semi-automatic verification tool based on a sound JSIL separation logic;
and verified axiomatic specifications of the JavaScript internal functions.
Using JaVerT, we verify functional correctness properties of:
data-structure libraries (key-value map, priority queue) written in an object-oriented style;
operations on data structures such as binary search trees (BSTs) and lists; examples illustrating function closures;
and test cases from the official ECMAScript test suite. The verification times suggest that reasoning about larger,
more complex code using JaVerT is feasible.
},
}
......@@ -1475,21 +1475,21 @@ more complex code using JaVerT is feasible.
year = {2015},
doi = {10.1007/978-3-319-28766-9_4},
project = { web },
abstract = {Client-side JavaScript programs often interact with the web page
into which they are included, as well as with the browser itself, through APIs
such as the DOM API, the XMLHttpRequest API, and the W3C Geolocation API.
Precise reasoning about JavaScript security must therefore take API invocation
into account. However, the continuous emergence of new APIs, and the heterogeneity
of their forms and features, renders API behavior a moving target that is particularly
hard to capture. To tackle this problem, we propose a methodology for modularly
extending sound JavaScript information flow monitors with a generic API.
Hence, to verify whether an extended monitor complies with the proposed noninterference
property requires only to prove that the API satisfies a predefined set of conditions.
In order to illustrate the practicality of our methodology, we show how an information
flow monitor-inlining compiler can take into account the invocation of arbitrary APIs,
without changing the code or the proofs of the original compiler.
We provide an implementation of such a compiler with an extension for handling a
fragment of the DOM Core Level 1 API. Furthermore, our implementation supports
abstract = {Client-side JavaScript programs often interact with the web page
into which they are included, as well as with the browser itself, through APIs
such as the DOM API, the XMLHttpRequest API, and the W3C Geolocation API.
Precise reasoning about JavaScript security must therefore take API invocation
into account. However, the continuous emergence of new APIs, and the heterogeneity
of their forms and features, renders API behavior a moving target that is particularly
hard to capture. To tackle this problem, we propose a methodology for modularly
extending sound JavaScript information flow monitors with a generic API.
Hence, to verify whether an extended monitor complies with the proposed noninterference
property requires only to prove that the API satisfies a predefined set of conditions.
In order to illustrate the practicality of our methodology, we show how an information
flow monitor-inlining compiler can take into account the invocation of arbitrary APIs,
without changing the code or the proofs of the original compiler.
We provide an implementation of such a compiler with an extension for handling a
fragment of the DOM Core Level 1 API. Furthermore, our implementation supports
the addition of monitor extensions for new APIs at runtime.},
}
......@@ -1506,14 +1506,14 @@ more complex code using JaVerT is feasible.
year = {2015},
doi = {10.1007/978-3-319-28766-9_5},
project = { web },
abstract = {As JavaScript is highly dynamic by nature, static information
flow analyses are often too coarse to deal with the dynamic constructs of
the language. To cope with this challenge, we present and prove the soundness
of a new hybrid typing analysis for securing information flow in a JavaScript-like language.
Our analysis combines static and dynamic typing in order to avoid rejecting programs
due to imprecise typing information. Program regions that cannot be precisely
typed at static time are wrapped inside an internal boundary statement used
by the semantics to interleave the execution of statically verified code
abstract = {As JavaScript is highly dynamic by nature, static information
flow analyses are often too coarse to deal with the dynamic constructs of
the language. To cope with this challenge, we present and prove the soundness
of a new hybrid typing analysis for securing information flow in a JavaScript-like language.
Our analysis combines static and dynamic typing in order to avoid rejecting programs
due to imprecise typing information. Program regions that cannot be precisely
typed at static time are wrapped inside an internal boundary statement used
by the semantics to interleave the execution of statically verified code
with the execution of code that must be dynamically checked.},
}
......@@ -1636,17 +1636,17 @@ invariants used to restrict the interference, and apply our reasoning to the exa
year = {2019},
project = { web },
doi = {10.1145/3290379},
abstract = { We propose a novel, unified approach to the development
abstract = { We propose a novel, unified approach to the development
of compositional symbolic execution tools, bridging
the gap between classical symbolic execution and compositional program reasoning
based on separation logic. Using this approach, we build JaVerT 2.0, a symbolic analysis tool for JavaScript
that follows the language semantics without simplifications. JaVerT 2.0 supports whole-program symbolic
testing, verification, and, for the first time, automatic compositional testing based on bi-abduction.
The meta-theory underpinning JaVerT 2.0 is developed modularly, streamlining the proofs and informing the
implementation. Our explicit treatment of symbolic execution errors allows us to give meaningful feedback
to the developer during wholeprogram symbolic testing and guides the inference of resource of the bi-abductive
execution. We evaluate the performance of JaVerT 2.0 on a number of JavaScript data-structure libraries,
demonstrating: the scalability of our whole-program symbolic testing; an improvement over the state-of-the-art
the gap between classical symbolic execution and compositional program reasoning
based on separation logic. Using this approach, we build JaVerT 2.0, a symbolic analysis tool for JavaScript
that follows the language semantics without simplifications. JaVerT 2.0 supports whole-program symbolic
testing, verification, and, for the first time, automatic compositional testing based on bi-abduction.
The meta-theory underpinning JaVerT 2.0 is developed modularly, streamlining the proofs and informing the
implementation. Our explicit treatment of symbolic execution errors allows us to give meaningful feedback
to the developer during wholeprogram symbolic testing and guides the inference of resource of the bi-abductive
execution. We evaluate the performance of JaVerT 2.0 on a number of JavaScript data-structure libraries,
demonstrating: the scalability of our whole-program symbolic testing; an improvement over the state-of-the-art
in JavaScript verification; and the feasibility of automatic compositional testing for JavaScript.},
}
......@@ -1731,9 +1731,10 @@ author = {Jos{\'{e}} {Fragoso Santos} and Petar Maksimovi\'{c} and Sacha{-}{\
title = { Gillian, Part I: A Multi-language Platform for Symbolic Execution },
booktitle = { Proceedings of the 41st ACM SIGPLAN
International Conference on Programming Language Design and Implementation
(PLDI ’20), June 15–20, 2020, London, UK },
year = {2020},
(PLDI ’20), June 15–20, 2020, London, UK },
year = {2020},
doi = {10.1145/3385412.3386014},
project = { gillian },
abstract = { We introduce Gillian, a platform for developing symbolic
analysis tools for programming languages. Here, we focus on
the symbolic execution engine at the heart of Gillian, which
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment