NuSMV is a new implementation and extension of SMV symbolic model checker, aimed for a reliable verification of industrially sized designs. The objective of this project is to model the Java Bytecode instruction flow of a program. With this model we can automatically check if a program respects the secure information flow property, which means certifying that there is no information leakage.
Every day about 20000 flights sail through the skies of the United States. Online a huge amount of data is available regarding each one of these flights, including information on delays, cancellations and their causes. From this data it’s possible to compute a large number of different statistics on mean delays, probability of cancellation, most probable delay cause etc. based on a single airport, route or airline. For this reasons we decided to create Skynet. Skynet is an application capable of gathering data from the U.S. Department of Transportation website through a web scraper implemented inside of it. The data is then analyzed, processed and distributed on multiple database realized through MongoDB and Neo4j technologies, which are necessary to achieve a good tradeoff between performances, reliability and availability.
A TFTP protocol is a simple lockstep File Transfer Protocol which allows a client to get a file from or put a file onto a remote host. This C implementation is suitable for embedded systems or for machines with limited resources.
The aim of this project was to build a secure online version of the famous table game Connect Four. We implemented the application using C language and the OpenSSL libraries. We also formally proved the protocols used during the communication between client and server with the BAN Logic formalism.
This project was made as part of the exam ‘Progettazione Web’ during my Bachelor’s degree. The main goals were to build a web application that would let users create or participate to events of various categories. The application is inspired from the famous EventBrite portal which is one of the most used in this sector.