1,721,023 research outputs found
Primitives for Contract-based Synchronization
Full text linkWe investigate how contracts can be used to regulate the interaction between processes. To do that, we study a variant of the concurrent constraints calculus presented in [1], featuring primitives for multi-party synchronization via contracts. We proceed in two directions. First, we exploit our primitives to model some contract-based interactions. Then, we discuss how several models for concurrency can be expressed through our primitives. In particular, we encode the pi-calculus and graph rewriting
Towards a linear contract logic
No full textWe introduce a linear logic for contracts. The logic (called PCLLW) extends intuitionistic linear affine logic ILLW with a contractual implication connective, along the lines of Propositional Contract Logic (PCL). A proof system for PCLLW is presented, and it is shown sound and complete with respect to a phase structure model. By exploiting the finite model property, we show that PCLLW is decidable
A Calculus of Contracting Processes
Full text linkWe propose a formal theory for contract-based computing. A contract is an agreement stipulated between two or more parties, which specifies the duties and the rights of the parties involved therein. We model contracts as formulae in an intuitionistic logic extended with a "contractual" form of implication. Decidability holds for our logic: this allows us to mechanically infer the rights and the duties deriving from any set of contracts. We embed our logic in a core calculus of contracting processes, which combines features from concurrent constraints and calculi for multiparty sessions, while subsuming several idioms for concurrency. We then show how to exploit our calculus as a tool for modelling services, the interaction of which is driven by contracts
Static Enforcement of Service Deadlines
Full text linkWe consider the problem of statically deciding when a service always provides its functionality within a given amount of time. In a timed pi-calculus, we propose a two-phases static analysis guaranteeing that processes enjoy both the maximal progress and the well-timedness properties. Exploiting this analysis, we devise a decision procedure for checking service deadlines
A brief tour of formally secure compilation
Full text linkModern programming languages provide helpful high-level abstractions and mechanisms (e.g. types, module, automatic memory management) that enforce good programming practices and are crucial when writing correct and secure code. However, the security guarantees provided by such abstractions are not preserved when a compiler translates a source program into object code. Formally secure compilation is an emerging research field concerned with the design and the implementation of compilers that preserve source-level security properties at the object level. This paper presents a short guided tour of the relevant literature on secure compilation. Our goal is to help newcomers to grasp the basic concepts of this field and, for this reason, we rephrase and present the most relevant results in the literature in a common setting
Type and Effects for Resource Usage Analysis
No full textAn extension of the -calculus is proposed, to study
resource usage analysis and verification.
Resources can be dynamically created, and passed / returned by functions;
their usages have side effects, represented by events.
Usage policies are properties over histories of events,
and have a possibly nested, local scope.
A type and effect system over-approximates the set of histories a program
can generate at run-time.
A crucial point solved here concerns correctly associating fresh resources
with their usages within approximations.
A second issue is that these approximations may contain an unbounded number of
fresh resources.
Despite of that, we have devised a technique to model-check validity of
approximations.
A program with a valid approximation is resource-safe:
no run-time monitor is needed to safely drive its executions
Local Policies for Resource Usage Analysis
No full textAn extension of the lambda-calculus is proposed, to study
resource usage analysis and verification.
It features usage policies with a possibly nested, local scope,
and dynamic creation of resources.
We define a type and effect system that, given a program, extracts
a history expression, i.e. a sound over-approximation to
the set of histories obtainable at run-time.
After a suitable transformation, history expressions are model-checked
for validity.
A program is resource-safe if its history expression is verified valid:
if such, no run-time monitor is needed to safely drive its executions
Explaining vulnerabilities of deep learning to adversarial malware binaries
Full text linkRecent work has shown that deep-learning algorithms for malware detection are
also susceptible to adversarial examples, i.e., carefully-crafted perturbations
to input malware that enable misleading classification. Although this has
questioned their suitability for this task, it is not yet clear why such
algorithms are easily fooled also in this particular application domain. In
this work, we take a first step to tackle this issue by leveraging explainable
machine-learning algorithms developed to interpret the black-box decisions of
deep neural networks. In particular, we use an explainable technique known as
feature attribution to identify the most influential input features
contributing to each decision, and adapt it to provide meaningful explanations
to the classification of malware binaries. In this case, we find that a
recently-proposed convolutional neural network does not learn any meaningful
characteristic for malware detection from the data and text sections of
executable files, but rather tends to learn to discriminate between benign and
malware samples based on the characteristics found in the file header. Based on
this finding, we propose a novel attack algorithm that generates adversarial
malware binaries by only changing few tens of bytes in the file header. With
respect to the other state-of-the-art attack algorithms, our attack does not
require injecting any padding bytes at the end of the file, and it is much more
efficient, as it requires manipulating much fewer bytes
- …
