Biblio

In this paper, we consider the runtime verification problem of safety hyperproperties for deterministic programs. Several security and information-flow policies such as data minimality, non-interference, integrity, and software doping are naturally expressed formally as safety hyperproperties. Although there are monitoring results for hyperproperties, the algorithms are very complex since these are properties over set of traces, and not over single traces. For the deterministic input-output programs that we consider, and the specific safety hyperproperties we are interested in, the problem can be reduced to monitoring of trace properties. In this paper, we present a simpler monitoring approach for safety hyperproperties of deterministic programs. The approach involves transforming the given safety hyperproperty into a trace property, extracting a characteristic predicate for the given hyperproperty, and providing a parametric monitor taking such predicate as parameter. For any hyperproperty in the considered subclass, we show how runtime verification monitors can be synthesised. We have implemented our approach in the form of a parameterised monitor for the given class, and have applied it to a number of hyperproperties including data minimisation, non-interference, integrity and software doping. We show results concerning both offline and online monitoring.

The fifth generation of mobile technology (5G) is positioned to address the demands and business contexts of 2020 and beyond. Therefore, in 5G, there is a need to push the envelope of performance to provide, where needed, for example, much greater throughput, much lower latency, ultra-high reliability, much higher connectivity density, and higher mobility range. A crucial point in the effective provisioning of 5G Next Generation Mobile Networks (NGMN) lies in the efficient error control and in more details in the utilization of Forward Error Correction (FEC) codes on the application layer. FEC is a method for error control of data transmission adopted in several mobile multicast standards. FEC is a feedback free error recovery method where the sender introduces redundant data in advance with the source data enabling the recipient to recover from different arbitrary packet losses. Recently, the adoption of FEC error control method has been boosted by the introduction of powerful Application Layer FEC (AL-FEC) codes. Furthermore, several works have emerged aiming to address the efficient application of AL-FEC protection introducing deterministic or randomized online algorithms. In this work we propose a novel AL-FEC scheme based on online algorithms forced by the well stated AL-FEC policy online problem. We present an algorithm which exploits feedback capabilities of the mobile users regarding the outcome of a transmission, and adapts the introduced protection respectively. Moreover, we provide an extensive analysis of the proposed AL-FEC algorithm accompanied by a performance evaluation against common error protection schemes.