Active areas:
Security of smart vehicular systems, and smart traffic control systems.
Privacy by design: automated and formal modeling and verification of data protection policies and architectures.
Children-related data privacy and online safety
a funded project called ChildDataVerif
Zero-trust architecture-based security solutions.
Air quality measurement based on participatory sensing.
AirSenSei Porject: Air Quality Sensor Network at School for Education Purposes (Funded by the DigitalLife Centre)
Near optimal cybersecurity investment solutions for businesses.
paper 1, toolkit (CyberOP/INspIRE)
Blockchain-based privacy and GDPR auditing framework.
paper 1, verification engine code
TTP-based cyber resilient index.
report 1, tool (TTPCRI)
In the past:
Automated verification of security API . Hardware Security Modules (HSM) are indispensable in many applications, such as ATM networks, public key infrastructures, electronic ticketing in public transportation, electronic payment systems, and electronic commerce, in general. A HSM is a hardware device (including the firmware and software components) which has some tamper resistance properties, and it is used to store cryptographic keys and to perform various security-critical cryptographic operations. Besides physical tampering and side channel attacks, HSMs can also be attacked through their APIs by exploiting some design weaknesses in the API's logic. Being fully software based, this kind of attacks is much less expensive than physical and side-channel attacks, and depending on the weaknesses that are exploited, it may have devastating effects. One promising approach of API analysis is to apply some formal verification method such as those used in software engineering. We follow this approach, and propose an API verification method based on the applied pi-calculus that seems to be extremely well-suited for the formal modeling of security APIs, the precise definition of the security requirements, and the rigorous analysis of the provided security properties. We demonstrate our approach through the analysis of the SeVeCom HSM API.
Automated security verification of firewalls. Firewalls are routinely used today to protect internal networks from attacks originating from the Internet. However, firewalls are often misconfigured leaving security holes in the defense system. As firewalls can be stateful and firewall rule sets may contain a very large number of rules, such misconfigurations are hard to discover by informal analysis. We are investigating how formal verification techniques can be used to alleviate this problem.
Formal and Automatic security verification of secure routing protocols. Ad-hoc networks are not based on pre-defined topology, thus, before each data exchange a route discovery is accomplished. The route discovery procedures are defined by routing protocols. Numerous attacks against routing protocols have been published, in which the attacker can achieve that the honest nodes attempt to exchange data through the route that does not exist. This type of attacks is critical because they can lead to futile energy consumption and degrade the efficiency of the network.
Query Auditing in Statistical Databases. In remote patient monitoring applications, sensor readings are collected on personal mobile device, such as a mobile phone. Third parties can then access these database sending queries to the mobile device. In order to preserve the privacy of users, the mobile device should enforce some access control policy that prevents statistical disclosure of private information. A technique to achieve this is auditing the queries and denying to respond if the response can be used to compute private information, such as the health status of the patients. The goal of the research project is to design and implement such a query auditing algorithm on a mobile platform.
Formal and Automated Security Verification of Transport Protocols. We address the problem of formal and automated security verification of WSN transport protocols that may perform cryptographic operations. The verification of this class of protocols is difficult because they typically consist of complex behavioral characteristics, such as real-time, probabilistic, and cryptographic operations. To solve this problem, we propose a probabilistic timed calculus for cryptographic protocols along with an automatic verification method, and demonstrate how to use them for proving security or vulnerability of protocols.