Tag Archives: Abstract interpretation

10/10/2018 – Talk by Gianluca Caiazza

Title: Supporting security of robotic software: access control policies and immutablezation of log records
Time: 14:30
Location: Meeting Room B, Building Zeta
Type: Research talk
Speaker:  Gianluca Caiazza
Abstract:  Security of robotics systems, as well as of the related middleware infrastructures, is a critical issue for industrial and domestic IoT applications, and it needs to be continuously assessed throughout the whole development lifecycle. Furthermore, logging is crucial in robotics research, providing prolonged insights into a robot’s situational understanding, progression of behavioral state, and resulting outcomes. Such recordings are invaluable when debugging complex robotic applications or profiling experiments ex post facto. The next generation open source robotic software stack, ROS2, is now targeting support for Secure DDS, providing the community with valuable tools for secure real world robotic deployments. However, given the growing number of high profile public incidents involving self-driving automotives, resulting in fatality or regulatory policy making, it is paramount that the integrity, authenticity and non-repudiation of such system logs are maintained to ensure accountability. Being mobile cyberphysical systems, robots present new threats and vulnerabilities beyond traditional IT: unsupervised physical system access or postmortem collusion between robot and OEM could result in the truncation or alteration of prior records. In this seminar, we discuss a framework for procedural provisioning access control policies for robotic software, as well as for verifying the compliance of generated transport artifacts and decision point implementations. Moreover, we address immutablezation of log records via integrity proofs and distributed ledgers with special consideration for mobile and public service robot deployments.

Alert: the seminar has been rescheduled from 13:30 to 14:30

11/07/2018 – Talk by Martina Olliaro

Title: M-String Segmentation: a Refined Abstract Domain for String Analysis in C programs
Time: 13:00
Location: Meeting room B, Building Zeta
Type: Research Result
Speaker:  Martina Olliaro
Abstract: We present a refined segmentation abstract domain for the analysis of strings in the C programming language, properly extending the parametric segmentation approach to array representation introduced by P. Cousot et al. to the case of text values. In particular, we capture the so-called string of interest of an array of char, in order to distinguish well-formed string arrays. A concrete and abstract semantics of the main C header file string.h functions are worked out in full detail.

18/01/2018 – Talk by Amit Mandal

Title: Vulnerability Analysis of Android Auto Infotainment Apps
Time: 13:00
Location: Meeting room B, Building Zeta
Type: Research result
Speaker:  Amit Mandal
Abstract: With over 2 billion active mobile users and a large array of features, Android is the most popular operating system for mobile devices. Android Auto allows such devices to connect with an in-car compatible infotainment system, and it became a popular choice as well. However, as the trend for connecting car dashboard to the Internet or other devices grows, so does the potential for security threats. In this paper, a set of potential security threats are identified, and a static analyzer for the Android Auto infotainment system is presented. All the infotainment apps available in Google Play Store have been checked against that list of possible exposure scenarios. Results show that almost 80% of the apps are potentially vulnerable, out of which 25% poses security threats related to execution of JavaScript.
[paper just presented at ACM Computing Frontiers 2018]

27/04/2016 – Tutorial day

Tutorial day

The ACADIA research centre organisms a tutorial day on hot topics in computer science.
Date: 27/04/2016
Location: Conference room, building Alpha, Scientific campus


– 11:00-13:00  Dale Miller (Ecole Polytechnique, Paris, France): “Communicating and trusting formal proofs”

– 14:00-17:00 Young Im Cho (Gachon Univ., Seoul, Korea): “Intelligent IoT Platforms for Smart City”

Abstract 1 (Communicating and trusting formal proofs)

In the mist of feeling insecure with our electronic communications, we can take solace in the advice that we can “trust the math” behind cryptography. Faced with concerns over the safety of fly-by-wire planes and self-driving cars, we should be able to find solace in the fact that some parts of our safety critical systems have been proved formally correct: that is, we should be able to “trust the proof”. The
way formal proofs are built today, however, makes trusting them difficult. While proof assistants are used to build formal proofs, those proofs are often locked to that assistant. Formal proofs produced by one proof assistant cannot usually be checked and trusted by another proof assistant nor by a future version of itself. Thus, one of the components of the scientific method that ensures trust-reproducibility – is missing from proof checking.
The field of proof theory, as initiated by Gentian in the 1930’s, has identified a great deal of structure in formal proofs. Given recent developments in this topic, it is now possible to apply what we know
about proofs in theory to what we would like to have for proofs in practice. To that end, I will present the Foundational Proof Certificates framework for defining the semantics of proof evidence.
Since such definitions are executable, it is possible to build proof checkers that can check a wide range of formal proofs. In this scheme, the logic engine that executes such definitions is the only thing that needs to be trusted. Since such a logic engine is based on well-known computational logic topics, anyone can write a logic engine in their choice of programming language and hardware in order for them to build a checker they can trust. I will also overview some of the consequences of defining proofs in this manner: provers can become networked far more richly than they are currently and both libraries and marketplaces of proofs are enabled in a technology independent


Abstract 2 (Intelligent IoT Platforms for Smart City)

Machine-to-Machine communications (M2M) is a phenomenon that has been proceeding quietly in the background, and it is coming into the phase where explosion of usage scenarios in businesses will happen. Sensors, actuators, RFID/NFC tags, vehicles, and intelligent machines all have
the ability to communicate. The number of M2M connections is continuously increasing, and it has been predicted to see billions of machines interconnected in a near future. M2M applications provide
advantages in various domains from building, energy, healthcare, industrial, transportation, retail, security to environmental services. This fast-growing ecosystem is leading M2M towards a promising future, however M2M market expansion opportunities are not straight forward.
M2M is suffering from the highly fragmented vertical domain specific approach, which has increased the R&D cost in each specific domain. In fact, various vertical M2M solutions have been designed independently and separately for different applications, which inevitably impacts or even impedes large-scale M2M deployment. The existence of multiple manufacturers, the lack of a common M2M Service Capability Layer and no clarity about what can be achieved have all combined to leave the field of M2M communications closer to dream than reality.
To reduce the standardization gap which exist between M2M domains, the ETSI Technical committee M2M defined an end to end M2M service platform with the intermediate service layer that are key components of the horizontal M2M solution. This standards based platform follows a RESTful approach with open interfaces to enable developing services and applications independently of the underlying network, thus easing the deployment of vertical applications for an effective interoperability, and facilitating innovation across industries.
The following topics will be covered by the tutorial:
– IoT basics
– Smart City basics
– IoT international platform focusing on OneM2M reference model
– Components and model description for IoT platform
– Examples in detail
– Case studies and demonstration etc.