A5077037306- Logic, programming, and type systems
- Security and Verification in Computing
- Logic, Reasoning, and Knowledge
- Formal Methods in Verification
- Access Control and Trust
- Advanced Authentication Protocols Security
- Distributed systems and fault tolerance
- Web Application Security Vulnerabilities
- Advanced Malware Detection Techniques
- User Authentication and Security Systems
- Cryptography and Data Security
- Advanced Database Systems and Queries
- Spam and Phishing Detection
- semigroups and automata theory
- Model-Driven Software Engineering Techniques
- Semantic Web and Ontologies
- Cryptographic Implementations and Security
- Artificial Intelligence in Games
- Software Engineering Research
- Mobile Agent-Based Network Management
- Cloud Data Security Solutions
- Petri Nets in System Modeling
- Advanced Software Engineering Methodologies
- Service-Oriented Architecture and Web Services
- Advanced Algebra and Logic
Università di Camerino
2023
Ca' Foscari University of Venice
2010-2019
Torino e-district
2005
University of Padua
1993-1999
Medidata (United States)
1990
Boxed Ambients are a variant of Mobile that result from dropping the open capability and introducing new primitives for ambient communication. The model communication is faithful to principles distribution location-awareness Ambients, complements constructs in out mobility with finer-grained mechanisms interaction. We introduce calculus, study impact typing mobility, show they yield an effective framework resource protection access control distributed systems.
Content Security Policy (CSP) is an emerging W3C standard introduced to mitigate the impact of content injection vulnerabilities on websites. We perform a systematic, large-scale analysis four key aspects that effectiveness CSP: browser support, website adoption, correct configuration and constant maintenance. While support largely satisfactory, with exception few notable issues, our unveils several shortcomings relative other three aspects. CSP appears have rather limited deployment as yet...
Session cookies constitute one of the main attack targets against client authentication on Web. To counter these attacks, modern web browsers implement native cookie protection mechanisms based HttpOnly and Secure flags. While there is a general understanding about effectiveness t hese defenses, no formal result has so far been proved security guarantees they convey. With present paper we provide first such result, by presenting mechanized proof noninterference assessing robustness flags...
Secure Safe Ambients (SSA) are a typed variant of [9], whose type system allows behavioral invariants ambients to be expressed and verified. The most significant aspect the is its ability capture both explicit implicit process ambient behavior: types account not only for immediate behavior, but also behavior resulting from capabilities acquires during evolution in given context. Based on that, provides static detection security attacks such as Trojan Horses other combinations malicious...
Content Security Policy (CSP) is a recent W3C standard introduced to prevent and mitigate the impact of content injection vulnerabilities on websites. In this article, we introduce formal semantics for latest stable version standard, CSP Level 2. We then perform systematic, large-scale analysis effectiveness current deployment, using substantiate our methodology assess detected issues. focus four key aspects that affect CSP: browser support, website adoption, correct configuration, constant...
Browser-based defenses have recently been advocated as an effective mechanism to protect web applications against the threats of session hijacking, fixation, and related attacks. In existing approaches, all such ultimately rely on client-side heuristics automatically detect cookies containing information, then them theft or otherwise unintended use. While clearly crucial effectiveness resulting defense mechanisms, these not, yet, undergone any rigorous assessment their adequacy. this paper,...
Enforcing protection at the browser side has recently become a popular approach for securing web authentication. Though interesting, existing attempts in literature only address specific classes of attacks, and thus fall short providing robust foundations to reason on authentication security. In this paper we provide such foundations, by introducing novel notion session integrity, which allows us capture many attacks spot some new ones. We then propose FF+, security-enhanced model that...
Browser-based defenses have recently been advocated as an effective mechanism to protect potentially insecure web applications against the threats of session hijacking, fixation, and related attacks. In existing approaches, all such ultimately rely on client-side heuristics automatically detect cookies containing information, then them theft or otherwise unintended use. While clearly crucial effectiveness resulting defense mechanisms, these not, yet, undergone any rigorous assessment their...
We propose a type and effect system for authentication protocols built upon tagging scheme that formalizes the intended semantics of ciphertexts. The main result is validation each component in isolation provably sound fully compositional: if all protocol participants are i ndependently validated, then as whole guarantees presence Dolev–Yao intruders possibly sharing long term keys with honest principals. Protocols thus validated both malicious outsiders compromised insiders. highly...
The challenges hidden in the implementation of high-level process calculi into low-level environments are well understood [3]. This paper develops a secure typed pi calculus, which capability types employed to realize policies for access communication channels. Our compiles processes pi-calculus principals cryptographic calculus based on applied-pi [1]. In this translation, type capabilities implemented as term protected by encryption keys only known intended receivers. As such, is effective...
Connectivity and communication interference are two key aspects in mobile ad-hoc networks (MANETs). We propose a process algebraic model targeted at the analysis of both such MANETs. The framework includes probabilistic calculus suite analytical techniques based on observational congruence an interference-sensitive preorder. allows us to verify whether exhibit same behaviour. preorder makes it possible evaluate level different, behaviourally equivalent, networks. show our work well-known...
Type systems for authorization are a popular device the specification and verification of security properties in cryptographic applications. Though promising, existing frameworks exhibit limited expressive power, as underlying languages fail to account powerful notions based on access counts, usage bounds, mechanisms resource consumption, which instead characterize most modern online services We present new type system that features novel combination affine logic, refinement types, types...