Fabio Massacci

• 1.1Academic degrees (M.Sc., Ph.D., etc.)

• 1998/Jun. - Univ. of Rome I "La Sapienza", PhD in Computer Science and Engineering. Thesis on automated reasoning for modal and security logics
• 1995/Mar. 95 – Master in International Affairs by SIOI and Ministry of Defence. Thesis on the relationship between Democracy and fundamentalist Islam.
• 1993/Nov. 93 - Univ. of Rome "La Sapienza", Master Degree in Computer Engineering. Thesis on automated autoepistemic reasoning.

• 1.2Habilitations

• 2003/Dec – Habilitation as full professor
• 1999/Mar - Habilitation as United Nations Officer – Level P2
• 1995/Mar - Ordine degli Ingegneri – Habilitation as Chartered Engineer

1.1     Present Position:

• Prof. Ordinario (Full Professor) at University of Trento – since 3/Jan/2005

1.2     Previous Employments

• 2001/Sep à 2005/Jan - Associate Professor, Faculty of Engineering, University of Trento – Italy
• 1999/Feb à 2001/Aug - Assistant Professor, Faculty of Engineering, University of Siena – Italy
• 1998/Jan à 1999/Feb - Postdoctoral Fellow, CNR, Rome, Italy
• 1997/Nov à1998/Dec –Research Assoc. on project by ASI (Italian Space Agency), U. of Roma "La Sapienza"
• 1994/Nov à 1997/Nov - PhD Fellowship at the University of Rome “La Sapienza”

1.3     Professional Appointments

• à now: Rector’s delegate for international ranking

• 2015/Oct à 2019/Feb – Deputy Head of School, Coordinator of Teaching – Dipartimento Ingegneria e Scienze dell’Informazione – Univ. of Trento.
• 2011/Jan à 2012/Jan – Vice Director for Education – TrentoRISE (EIT – ICTLabs Italy)
• 2002/Mar à 2008/sep – Deputy Rector for ICT Services – University of Trento – Italy
  • Supervision of IT department and its CIO (including performance target), budget 3M€/year, staff 70 people, outsourcing contracts for Metrop. Area Network, ERP system (SAP), and education portal.

1.4     Visiting appointments

• 2020/21 – Winter Term –Institute for Advanced Studies Fellow – Durham University, UK
• à2017/Jul – ISI University of Southern California  – Los Angeles, USA
• à2016/Jul – (1m/yr) - Durham Business School  – Durham, UK
• à2013/May – Visiting Researcher – KULeuven, Leuven, Belgium
• 2012/Jun à 2012/Aug – DIMACS – special program on Cybersecurity, Rutgers, USA
• 2007/Jan à 2012/Apr – Guest Scientist for the DIGIT Project – SINTEF, Oslo - Norway
• 2005/Jan à 2009/Dec – Guest Scientist for the ENFORCE Project – SINTEF, Oslo – Norway
• 2000/Jun à 2000/Dec - Visiting Researcher - IRIT - CNRS, Toulouse – France
• 1996/Feb à 1997/Feb - Visiting Student, Computer Laboratory, Univ. of Cambridge – UK

I illustrate below some of the major milestones in my research with some sample papers. They are not necessarily the most cited; they are the ones that one could actually read to have a comprehensive idea of my research.

More details are available in the Research and Teaching Statement.

Empirical Security Economics: My current research effort is to empirically validate practical and affordable security solution, albeit they might not be perfect. Often security solutions stop at a mathematical model, we go the last mile (more precisely the last light year) and empirically validate them by running experiments or by performing qualitative studies. Such works often go against the “ethos” of academic security research working to protect us against an all powerful adversary, yet it has an unfettered potential of industry impact (you can better prioritize your finite resources instead fighting an all powerful adversary that doesn’t exist). Three papers illustrate this research, two in flagship computer security venue and one in a top business journal.

1. Allodi, L, Massacci, F. Comparing vulnerability severity and exploits using case-control studies. ACM Trans. on Information and System Security, 17(1):1 (2014).  The conference version was rejected several times (ICSE, CCS, ESORICS, etc.) because “It is just bad scholarship to suggest that one should not worry about all vulnerabilities”. People in industry knew better (they invited us at BlackHat USA 2013), as they know too well that their budget is fixed and therefore the academic advice of worrying about all vulnerabilities is useless. We looked at data from Symantec and black markets, combined it with solid mathematical research on statistics and risk reduction and we identified the vulnerabilites one should worry about. The outcome made up to the CVSS world standard. Out of this research we also made available to the community several databases licensed to Fraunhofer, MITRE, NCSU, MIT Sloan, MIT Lincoln Lab among others.
2. De Gramatica, M., Massacci, F., Shim, W., Turhan, U. & Williams, J. (2016). Agency Problems and Airport Security: Quantitative and Qualitative Evidence on the Impact of Security Training. Risk Analysis 2017. This paper evaluates which type of security training is most effective for airport security officers (training costs >900€/person). We have a solid model based on principal-agent theory and validated it with interviews with high profile stakeholders. We transformed a “gut feeling” into an actionable model. The results were presented to ACI Europe, the federation of European Airport Directors.
3. Massacci, F., Ngo, C. N., Nie, J., Venturi, D., & Williams, J. FuturesMEX: secure distributed futures market exchange. Proceedings of IEEE Symposium on Security and Privacy. 2018. This is a joint paper with economists and cryptographers: how to run a exchange like the Chicago Mercantile Exchange in a distributed fashion. We solved an already solved problem (an exchange is just an example of multi party computation -MPC), except that we did in a way that it was solvable with real empirical data. By using MPC even from top theory papers not only running a small market like Lean Hog trades would have required an year to just run a day of trading, but, to add insult to injury, retail and institutional investors (who only do 20% of the trades) would have had to spend 80% of the overall computational resources to allow high-frequency traders to place speculative orders that would have then been almost immediately canceled. When my business colleague J. Williams presented the paper and our patents in China to hedge funds he expected 20 people. He had 200.

Security Requirements Engineering: I started this work in 2003 with N. Zannone and J. Mylopoulos. The key idea is to  develop a robut methodology to capture security requirements as first class citizens. Two, very different, ten-years apart, papers illustrate this research: initially I worked on design and formal reasoning capabilities, now understanding what really works in security risk analysis is the other focus in my research that complements it.

1. Giorgini P., Massacci F., Mylopoulos J., Zannone N., "Requirements Engineering for Trust Management: Model, Methodology, and Reasoning". Int. J. of Information Security, 5(4):257-274, 2006. The short version of this paper appeared in IEEE RE’2005 and received in 2015 the Ten Years Most Influential Paper Award by the IEEE Requirements Engineering Conference. In this paper we designed a security methodology to capture security requirements, an underlying formalization in terms of logic programs and a verification methodology that would check whether desirable security properties would be satified.
2. De Gramatica M, Labunets K, Massacci F, Paci F, Tedeschi A. The Role of Catalogues of Threats and Security Controls in Security Risk Assessment: An Empirical Study with ATM Professionals. In Proc. of the Int. Conf. on Req. Engineering: Foundation for Software Quality (REFSQ). 2015. So, we invented a “super-duper” security requirements method, why did industry not flock to adopt it? Since 2010, I have been experimenting to understand what works in practice. For example, in this paper with an industry co-author, we focus on catalogues: academic methods never have them, industry works with catalogues of several hundred pages (eg the NIST-800-x and ISO-2700x). They do make the difference between novices and experts. Understanding what makes a research method empirically usable by somebody else than its inventor is the pre-requisite for successful innovation.

Run-time and load-time security enforcement. This research is a mixture of theoretical research on the limit of what can be actually enforced and what can be practically achieved. Out of this research stream started my long standing collaboration with KU Leuven (F. Piessens and Wouter Josen).

1. Ngo M., Massacci F., Milushev D., Piessens F.. “Runtime Enforcement of Security Policies on Black Box Reactive Programs”. In Proc. of the 42nd ACM Symp. on Principles of Progr. Lang.. POPL’2015. This paper summarizes the theoretical investigation on the limit and power of run-time enforcement mechanisms. With another students, N. Bielova we investigated the limits of edit automata (IJIS, JCS and POLICY’11) showing that practical enforcement cannot be simply caputred by the two basic concept of transparency and soundness.
2. Desmet L, Joosen W., Massacci F., Philippaerts P., Piessens F., Siahaan I., Vanoverberghe D. Security-by-contract on the .NET platform. Inform. Security Technical Rep.13 (1):25-32, Jan 2008. This is one of the first papers describing the formal security checking of apps on a mobile phones. It is a comprehensive paper spannign from theory to implementation. We could run a checker testing whether an app respected some security policies. On the same year US  researchers proposed at CCS to use very simple checks on android apps and could onlyuse the manifest of the app, we used real code. Our industry partner of the S3MS project, DoCoMo, licensed the industrial application in Japan and I tried to negotiate with Vodafone Itay its commercialization. Alas, .NET and Microsoft lost to Android…
3. Koshutanski H., Massacci F.: Interactive access control for autonomic systems: From theory to implementation. ACM Trans. on Autonomous and Autonomic Systems 3(3): 2008. H. Koshutanski was my first “own” phd student in 2002 and started his research with a workshop paper that got significantly more citations than this final “round-up” journal. This paper summarizes our work on trust negotiation in which we combined a solid theory (abduction) with a running implementation (an opens source is available at http://www.interactiveaccess.org). This research is basically the only academic background of Microsoft’s patent US8060920 and Apple’s patent US8813185B2 on the dynamic management of users’ credentials.

Formal Methods for Security: In 1996, half-way through my Phd, I went to Cambridge to work with Robin Milner (one of the inventor of the Hennessy-Milner logic). Alas, Milner had just been elected head of department and suggested I could work with Roger Needham and Larry Paulson who had a joint project on modal logic for security. This “one year long mishap” gave a whole new turn to my research career.

1. Bella G., Massacci F., Paulson L.C,: Verifying the SET Purchase Protocols. J. of Automated Reasoning 36(1-2):5-37, 2006. This paper describes the first work ever of verification of a major industrial protocol. Up to that point most of the formal security verification papers where about breaking and fixing academic protocols whose description could fit in a single page. Security researchers woud claim that formal methods could not scale. SET (Secure Electronic Transactions) was VISA’s and Mastercard’s protocol for the web. Its specification was thicker than a dictionary. We proved it correct and put to rest any claim that formal methods could not scale, but the effort in terms of time and person months was far from push-button technologies...
2. Massacci F., Marraro L., "Logical Cryptanalysis as a SAT-Problem: Encoding and Analysis of the U.S. Data Encryption Standard". Journal of Automated Reasoning, 24(1-2):165-203, 2000. This research stemmed from a crazy idea I had when I returned from Cambridge. In the AI and formal method community SAT solvers were the new research fad that seemed to crack previously unsolvable problems. At the end of the day what is a cryptoraphic circuit? Just a big boolean formula. What is a cryptanalysis problem? Just a bit SAT problem. The devil is of course in the detail and managing to encode symmetric and public key crypto was far easy (for the latter it appeared in Discrete Applied Mathematics). We failed to crack real crypto and that time but SAT competitions still use crypto benchmarks today but Marc Stevens SHA-1 cracking in 2017 used a SAT solver of a MSc Student of mine (V. Nossum) as a major component..

Automated Resoning for Modal Logic: When I started my Phd, reasoning in modal logic was divided in two fields: those that purely manipulate formulas and those that manipulated the corresponding models. I tried to combine both ideas to get something better than both. The tableaux for modal and description logics that I did as single author or with a couple of colleagues revamped the area.

Massacci F., "Single Step Tableaux for Modal Logics". Journal of Automated Reasoning, 24(3): 319-364, 2000.  In the Handbook of Tableaux Methods (1999) the chapter on modal tableaux by Gorè devotes 30 pages to my CADE paper of the mid 90s (the journal version is the one reported here). In 2014 our works in the area are still cited. My greatest satisfaction is a paper in the volume in memoriam of H. Ganzinger by R. Schmidt and U. Hustadt, the recognized advocates of the scientific competitor of tableaux (translation+resolution). Their paper “First-Order Resolution Methods for Modal Logics” is a survey with 90+ citations. There are only 2 citations for tableaux: the handbook above and one of my papers. I left the field 15 years ago and a citation by a scientific “enemy” to a paper 10 years old is truly “l’honneur des armes”.

1.1.1Summary of publications  (Data on 2019/Aug)

• Recent years highlights in Computing (CORE/ERA):
  • IEEE Transactions of Software Engineering (A*), ACM Transactions on Information and System Security (A), Empirical Software Engineering Journal (A), Journal of Systems and Software (A), ACM Symposium on Principles of Programming Languages (A*), IEEE Symposium on Security and Privacy (A*), ACM/IEEE Internat. Symp. on Empirical Software Engineering and Measurement (A)
• Recent years highlights in Business and management (CABS/Academic Journal Guide):
  • Risk Analysis (4)
• Recent highlights in Professional security conferences
  • BlackHat USA, BlackHat Asia
• Raw Data
  • Journal Papers: 48 (17 in the past 5 years)
  • Conference and Workshop papers: 138 (20 in the past 5 years)
  • Edited Books and Journals: 11
  • Professional Peer-reviewed Journal Article: 2
  • Book Chapters: 10
  • Italian Books: 2
  • Patents: 1 (3 submitted in 2018)

1.1.1Summary of grants (as PI)

• EU Pilot on CyberSecurity Network and Centre (Site leader)UniTN Funding: 0.45M€
• EU Projects as Admin. EU Coordinator: 2 STREPs and 1 IP UniTN Funding:1.81M€
• EU Projects as Scientific Coordinator: 1 IP UniTN Funding:0.92M€
• EU projects as Site Leader: 2 IP, 1 NoE, 2 CSA, 2 EIT(*)UniTN Funding:1.61M€
• National Projects as site leader: 1 MIUR, 1PAT, 1 ASIUniTN Funding:0.27M€
• Industry Grants: 2 EU, 1 National, 1 International UniTN Funding:0.60M€

(*) Excluding EIT funding for teaching I&E in security courses

1.1.2Industrial Impact

• Contributed to CVSS – Common Vulnerability Scoring Systems – The World Standard on vulnerabilities
• Work on risk- vs rule-based regulation presented by National Grid to the UK Cabine Office and EU Presidency

1.1.1Summary of supervised collaborators

• Graduated PhD students: 13 (BG, BY, ID, IT, UA, VN)
  • Started but dropped: 2 (BY, IT), changed advisor: 1 (IN), changed university: 2 (CO, BR)
• Current Phd students: 4 (RU, VN, IT)
• Postdoctoral researchers: 9 (CN, DE, FR, KR, ID, IT, RU)

1.1.2Current position of past collaborators

• Assistant professor, dozent, lecturer, and full professor: 6 (in CH, CN, DK, IT, NL, SE)
• Researcher at research centers: 3 (CNR – IT, INRIA - FR, KIPA - KR)
• International companies: 5 (ATOS, Bosch, Bromium, Google, WorldQuant)
• Public administration: 1 (CA)
• Senior developer in SME: 1 (IT)
• Post-doctoral researchers: 5 (CA, ID, LU, NL)

1.1.3Awards of PhD Students

• I. Pashchenko, 2017, 2^nd place at ESEC/FSE SRC Graduate Student Competition
• M. S. Tran, 2016. CAiSE PhD Award for Best Doctoral Dissertation
• L. Allodi, 2016. University of Trento Best Doctoral Dissertation

Member of the AEA, ACM, IEEE, ISACA, Society for Risk Analysis and Chartered engineer.

1.1     Scientific Awards.

• 2015/Aug – Ten Years Most Influential Paper Award by IEEE Requirements Engineering Conference for the paper: P. Giorgini, F. Massacci, J. Mylopoulos, N. Zannone: Modeling Security Requirements Through Ownership, Permission and Delegation. In Proc. of IEEE Requirements Engineering’05, p. 167-176, IEEE Press 2005.
• 2012/Jul – Best paper award at the IEEE International Conference on Cyber Security (CyberSecurity)
• 2001/Sep. – “Intelligenza Artificiale" career award by the Italian Association of Artificial Intelligence (AI*IA) for young researchers in AI under 35

More information on www.massacci.org