1,721,069 research outputs found
An Abstract Interpretation Framework for Type and Effect Systems
No full textType and effect systems significantly extend type systems and allow one to express general semantic properties and to statically reason about programs execution. They have been widely exploited to specify static analyses, for example to track computational side effects, resource usage and communication in concurrent languages. In this paper we adopt abstract interpretation techniques to express type and effect systems as abstract semantics. We extend the Cousot's methodology by introducing an abstract domain which (i) is able to express types with annotations, (ii) is reusable in different analyses with few modifications and (iii) is easily implementable. To test our approach we reconstruct two analyses for which the type and effect systems approach were successful
A Reconstruction of a Types-and-Effects Analysis by Abstract Interpretation
No full textAndartevelo a ceracr
Securing IoT communications: at what cost?
Full text linkIoT systems use wireless links for local communication, where locality depends on the
transmission range and include many devices with low computational power such as sensors.
In IoT systems, security is a crucial requirement, but difficult to obtain, because standard cryptographic techniques have a cost
that is usually unaffordable.
We resort to an extended version of the process calculus LySa, called IoTLySa,
to model the patterns of communication of IoT devices.
Moreover, we assign rates to each transition
to infer quantitative measures on the specified systems.
The derived performance evaluation can be exploited to
establish the cost of the possible security countermeasures
Tracking sensitive and untrustworthy data in IoT
Full text linkThe Internet of Things (IoT) produces and processes large amounts of data. Among
these data, some must be protected and others must be carefully handled because they
come from untrusted sources. Taint analysis techniques can be used to for marking data and for monitoring their propagation at run time, so to determine how they influence the rest of the computation.
Starting from the specification language IoT-LySa, we propose
a Control Flow Analysis for statically predicting how tainted data spread across an IoT system and for checking whether those computations considered security critical are not affected by tainted data
The cost of securing IoT communications
Full text linkMore smart objects and more applications on the Internet of Things (IoT) mean more security challenges. In IoT security is crucial but difficult to obtain. On the one hand the usual trade-off between highly secure and usable systems is more impelling than ever; on the other hand security is considered a feature that has a cost often unaffordable. To relieve this kind of problems, IoT designers not only need tools to assess possible risks and to study countermeasures, but also methodologies to estimate their costs. Here, we present a preliminary methodology, based on the process calculus IoT-LySa, to infer quantitative measures on systems evolution. The derived quantitative evaluation is exploited to establish the cost of the possible security countermeasures
Measuring security in IoT communications
Full text linkMore smart objects and more applications on the Internet of Things (IoT) mean more security challenges. In IoT security is crucial but difficult to obtain. On the one hand the usual trade-off between highly secure and usable systems is more impelling than ever; on the other hand security is considered a feature that has a cost often unaffordable. Therefore, IoT designers not only need tools to assess possible risks and to study countermeasures, but also methodologies to estimate their costs. Here, we present a methodology, based on the process calculus IoT-LySa, to infer quantitative measures on evolution of systems. The derived quantitative evaluation is exploited to establish the cost of the possible security countermeasures, in terms of time and energy
Analysing the Provenance of IoT Data
No full textThe Internet of Things (IoT) is leading to a smartification of our society: we are surrounded by many smart devices that automatically collect and exchange data of various kinds and provenance. Many of these data are critical because they are used to train learning algorithms, to control cyber-physical systems or to guide administrators to take decisions. Since the collected data are so important, many devices can be the targets of security attacks. Consequently, it is crucial to be able to trace data and to identify their paths inside a network of smart devices to detect possible threats. To help designers in this threat reasoning, we start from the modelling language IoT-LySa, and propose a Control Flow Analysis, a static analysis technique, for predicting the possible trajectories of data in an IoT system. Trajectories can be used as the basis for checking at design time whether sensitive data can pass through possibly dangerous nodes, and for selecting suitable security mechanisms that guarantee a reliable transport of data from sensors to servers using them. The computed paths are also interesting from an architectural point of view for deciding in which nodes data are collected, processed, communicated and stored
Resilience of Hybrid Casper under varying values of parameters
Full text linkHybrid Casper is the new Ethereum blockchain protocol that uses both Proof of Work and Proof of Stake to reach a consensus between nodes. Here, we analyse the protocol using PRISM+, an extension of the probabilistic model checker PRISM with primitives for expressing blockchain data types. First, we extend PRISM+ to include data types and operations for modelling and analysing Proof of Stake-based consensus protocols. Then, we model Hybrid Casper in PRISM+ as a parallel composition of stochastic processes, thus precisely describing the behaviour of the protocol and highlighting its corner cases. PRISM+ is therefore used to rapidly and automatically analyse the resilience of Hybrid Casper when tuning, up or down, several basic parameters of the protocol, such as the rates of creating blocks, and the strategies for determining penalties. Finally, we study the robustness of Hybrid Casper to two well known attacks: the Eclipse attack and the majority attack
Context-aware security: Linguistic mechanisms and static analysis
Full text linkAdaptive systems improve their efficiency by modifying their behaviour to respond to changes in their operational
environment. Also, security must adapt to these changes and policy enforcement becomes dependent on the dynamic contexts.
We study these issues within MLCoDa, (the core of) an adaptive declarative language proposed recently. A main characteristic
of MLCoDa is to have two components: a logical one for handling the context and a functional one for computing. We extend
this language with security policies that are expressed in logical terms. They are of two different kinds: context and application
policies. The first, unknown a priori to an application, protect the context from unwanted changes. The others protect the
applications from malicious actions of the context, can be nested and can be activated and deactivated according to their scope.
An execution step can only occur if all the policies in force hold, under the control of an execution monitor. Beneficial to this is
a type and effect system, which safely approximates the behaviour of an application, and a further static analysis, based on the
computed effect. The last analysis can only be carried on at load time, when the execution context is known, and it enables us to
efficiently enforce the security policies on the code execution, by instrumenting applications. The monitor is thus implemented
within MLCoDa, and it is only activated on those policies that may be infringed, and switched off otherwise
Here you can't: context-aware security.
Full text linkAdaptive systems improve their eciency by modifying their
behaviour to respond to changes of their operational environment. Also,
security must adapt to these changes and policy enforcement becomes
dependent on the dynamic contexts. We address some issues of context-
aware security from a language-based perspective. More precisely, we
extend a core adaptive functional language, recently introduced by some
of the authors, with primitives to enforce security policies on the code
execution. Then, we accordingly extend the existing static analysis in
order to insert checks in a program. The introduced checks guarantee
that no violation occurs of the required security policies
- …
