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.

6 open fully funded PhD positions in Computer Science. Deadline: April, 21st

Ca’ Foscari University, Venice, announces 6 open fully funded PhD position in Computer Science, one of which on the following specific subject:

- “Data Science”, funded by ZHAW (Zurich University of Applied Sciences) – School of Engineering (Switzerland). More information at http://www.zhaw.ch/datalab/teaching

PhD students will have the opportunity to do their work in one of the three well-established research centers:

- ACADIA (www.dais.unive.it/acadia)
- KIIS (www.dais.unive.it/kiis)
- Dhv (Digital Humanities Venice), in collaboration with EPF de Lausanne and Telecom Italia

The PhD students will be based in the modern scientific campus of Mestre (https://www.youtube.com/watch?v=QWTtdyHMu1A), reachable in only 10 minutes from Venice by public transportation. The campus is highly international with both Master and PhD courses completely held in English.

For more information please contact the program coordinator Prof. Riccardo Focardi (focardi@unive.it)

Application deadline is April, 21st 2016 1 PM (Italian time) and can be done on-line at:

- English: http://www.unive.it/nqcontent.cfm?a_id=173236
- Italian: http://www.unive.it/pag/7738/

See more info at this page

23/03/2016 – Talk by Renzo Derosas

Title:  Modelling a Demographic Suicide: the Venetian Aristocracy, 1500 to 1800.
Time: 14:30
Location: Meeting room, building Zeta
Type: Research Result
Speaker: Renzo Derosas
BACKGROUND: Around 1500, the Republic of Venice was a leading European power, ruling over an empire that stretched from the current Swiss and Austrian borders on the north, all along the Adriatic coast, to the islands of Cyprus and Crete in the southeast. Although its political regime was celebrated as a mix a democratic, aristocratic, and monarchical features, political power was the monopoly of a limited number of aristocratic families who passed it on from generation to generation. Indeed, Venice was defined “a republic of families”, whose destinies were fully identified with the State they belonged to. On the one hand, the very survival of the Republic depended on the reproduction – demographic, economic, and cultural – of its ruling class; on the other hand, there was hardly a place for the Venetian nobility without the State that supported its privileged status.
The number of aristocratic families grew from ca. 600 in 1400 to a maximum of 900 in 1500, and then declined steadily to a low of 350 at the fall of the Republic (1797). Correspondingly, the noblemen grew from 900 in 1400 to 2,650 in 1500, to fall to 1,100 in 1797. Although contemporaries were aware of the problems deriving from such a trend, all efforts to invert it turned out ineffective. Historians agree that the decline originated in the peculiar marriage policy adopted by the aristocracy: once Venetian nobles converted from merchants into landowners, they allowed only one male per generation to marry. They were obsessed with keeping their assets undivided, since any branching out would jeopardize their social and political standing. Unfortunately, the outcome was disastrous under both the demographic and the economic standpoints. At the fall of the Republic, due to the hazards of reproduction, almost two thirds of the families extinguished, while most of the survivors were heavily impoverished.

OBJECTIVES: With this research project, we challenge the current interpretation of the demographic decline of the Venetian aristocracy. We argue that it is incomplete, inasmuch it does not consider that many noblemen rather remained single than marry, condemning their families to extinction. Such a behavior was deeply contrary to the ethics and the ideology of the aristocracy. How can we explain it? Our aim is to develop a theory that accounts for both the decision to marry or not to marry.

METHODS: Our starting point is the assumption that marital choices in the Venetian aristocracy were primarily a political option, undertaken to enhance a family’s position in the political arena through the acquisition of new kin. More specifically, we hypothesize that, when it came to establish a new and lasting alliance through the marriage of their members, families strove to maximize their relational capital they would acquire. Our related hypothesis is that when the advantage deriving from all potential matches was below a certain threshold, a family would rather abstain from joining the market.
Although the strategic importance of marital choices by the Venetian aristocracy is largely circulating in the literature, the evidence provided thus far was only anecdotal and rather loosely defined. To test our hypothesis, we proceed in a tentative and exploratory way. Since we have only a list of the marriages celebrated along time but not of the population at risk, we define a set of potential partners made up by all those who married in the same year. We then outline the potential ego-networks formed by each match, and compute a series of centrality measures associated to each ego-network. Finally, we run a logistic regression to test whether any of such measures affects the likelihood of a match.

09/03/2016 – Talk by Stefano Calzavara

Title:  HornDroid: Practical and Sound Static Analysis of Android Applications by SMT Solving
Time: 13:30
Location: Meeting room, building Zeta
Type: Research Result
Speaker: Stefano Calzavara
We present HornDroid, a new tool for the static analysis of information flow properties in Android applications. The core idea underlying HornDroid is to use Horn clauses for soundly abstracting the semantics of Android applications and to express security properties as a set of proof obligations that are automatically discharged by an off-the-shelf SMT solver. This approach makes it possible to fine-tune the analysis in order to achieve a high degree of precision while still using off-the-shelf verification tools, thereby leveraging the recent advances in this field. As a matter of fact, HornDroid outperforms state-of-the-art Android static analysis tools on benchmarks proposed by the community. Moreover, HornDroid is the first static analysis tool for Android to come with a formal proof of soundness, which covers the core of the analysis technique: besides yielding correctness assurances, this proof allowed us to identify some critical corner-cases that affect the soundness
guarantees provided by some of the previous static analysis tools for Android.

02/03/2016 – Talk by Filippo Cavallin

Title:  Cronization: a method to pass from Continuous Time to Discrete Time Automata
Time: 14:00
Location: Meeting room, building Zeta
Type: Research Result
Speaker: Filippo Cavallin
Discrete and Continuous Time automata are important formalisms to model and analyze systems such queuing and telecommunication networks. The stationary performance analysis of these automata requires the computation of the steady-state distribution of their underlying Markov chains. Sometimes for the analysis is more convenient to pass from continuous to discrete time. The main methods are focused on the underlying Markov chains and not on the automatas. To preserve the transitions with labels and the synchronization between them, we will introduce a method to pass from a continuous time stochastic automaton (SA) to a probabilistic Input/Output automaton (PIOA). This method is a bijection from continuous to discrete time and it allows us to switch between the two different types of automata and it preserves the parallel composition.

25/01/2016 – Talk by Pierpaolo Degano

Title:  Context-aware Security: Linguistic Mechanisms and Static Analysis
Time: 14:00
Location: Meeting room, building Zeta
Type: Research Result
Speaker: Pierpaolo Degano
Adaptive 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 (the core of) an adaptive declarative language proposed recently. A main characteristic of this language is to have two components: a logical one for handling the context and a functional one for computing. We extend it 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 occur only 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 the language itself, and it is only activated on those policies that may be infringed and switched off otherwise.

Short bio
Pierpaolo Degano has been

  • since 1/11/1990 full Professore in computer science, since 1993 at Dipartimento di Informatica, Università di Pisa
  • 1993-96 head of the Dipartimento di Informatica, Università di Pisa
  • 2000-2003 Chairman of GRIN, the Italian Association of the Professors of Computer Science
  • since 2001 member of the scientific committee of the Scuola di Dottorato di Eccellenza “Galileo Galilei”, since 2009 vice-chairman
  • since 2006 head of the PhD programme in Computer Science
  • since 2007 chairman of the Italian Committee of PhD programmes in Computer Science
  • since 2005 member of the scientific committee of CoSBi, the Microsoft Research – University of Trento Centre for Computational and Systems Biology

22/01/2016 – Talk by Stefano Zanero

Title:  Making sense of a million samples per day: Behavior-based Methods for Automated, Scalable Malware Analysis
Time: 12:00
Location: Meeting room, building Zeta
Type: Research Result
Speaker: Stefano Zanero
With the astonishing rate of new and modified malware samples being released daily, automation of analysis is needed to classify and cluster together similar samples, exclude basic and uninteresting variations, and focus costly manual analysis work on novel and interesting features (e.g., added or remove pieces of code with a given semantic). We will discuss the challenges in analyzing large malware datasets in a (semi)automatic fashion, and some recent research results that may help with the task, by leveraging the concept of “behavior” applied to malicious code.
Short bio: Stefano Zanero is an associate professor at DEIB, the computer engineering department of the Politecnico di Milano University. His research interests focus on systems security, in particular automated malware analysis, cyber-phisical systems security, critical infrastructure security, as well as computer forensics.

16/12/2015 – Talk by Heider Wahsheh

Title:  Security Issues in Two Dimensional Barcodes
Time: 12:30
Location: Meeting room, building Zeta
Type: Survey
Speaker: Heider Wahsheh
A barcode is a graphical image that stores data in special patterns of black and white modules. The encoded data can be retrieved using imaging devices such as: barcode scanner machines and smart phones with specific reader applications. In general data can be stored in one dimension (horizontally), or two dimensions (both horizontally and vertically) with more data capacity. Barcodes are easy to use, free and very popular. Barcodes have various applications such as product tracking, advertising and items identification. However, attackers may use barcodes in a malicious way to launch attacks aiming at violating security and users’ privacy. This seminar presents various malicious scenarios with 2-D barcodes and possible protection mechanisms.

09/12/2015 – Talk by Mohamed Abbadi

Title:  ntroducing Casanova 2, a pragmatic domain specific language for game development
Time: 13:00
Location: Meeting room, building Zeta
Type: Research Results
Speaker: Mohamed Abbadi
The impact of video games, and games in general in our society is getting bigger and bigger to the point that game sales have passed those of music and movies (combined). Nowadays, video games are used not only for entertainment purpose, but also for serious applications such as research, education, training, etc.

Unfortunately, serious game development with traditional general-purpose programming language is a costly endeavor. The inherent complexity of the domain of videogames (physics simulation, AI, rendering, time management, etc.) is absolutely not tamed by typical programming languages. In these languages, we find no first class support of the flow time, lack of intelligent optimization mechanisms, and no understanding of the game loop. Since serious games developers do not enjoy the same resources as in the industry, taming costs of developing games is a very important necessity. Brilliant ideas might not see the light of day if there are not enough resources to support the development processes.

Here comes our work into play: in the past years a tool designed around the domain of games called Casanova has been designed and developed in order to: (i) allow innovative projects to see the end of their development process, (ii) provide developers with the right tool to tackle features that with limited resources might not be built, and (iii) keep the costs in check.
The Casanova programming language has the goal of offering a simple to use, high-performance, effective programming language that is capable of tackling the domain of videogame programming languages, from basic game logic programming up to strategies for AI.

In the presentation I will discuss my past Ph.D. experience and show the latest results of my research: different games for different genres, web-games, virtual-reality lab game, automatic optimizations, LegoV3/Casanova, and some students projects.

03/12/2015 – Talk by Marco Squarcina

Title:  Run-time analysis of PKCS#11 attacks
Time: 13:30
Location: Acadia Lab, building Zeta
Type: Research Results
Speaker: Marco Squarcina
The goal of this talk is to report on the development of a tool aimed at the automatic detection of attacks against PKCS#11 devices. Instead of modifying or configuring the API, we propose a stateful run-time monitor which is able to track key usage over time, for the identification of operations that might result in the leakage of sensitive keys. We briefly report on the components developed for implementing the monitor and discuss new challenges and open issues.