Forum Numerica - António Ravara : Most Cybersecurity vulnerabilities are software bugs!

Systems software is critical to our society's infrastructure but pervasively subject to security flaws and attacks; it is trusted but not trustworthy. All sorts of exploitable vulnerabilities and bugs appear in software, often leading to program crashes: 
- issues linked to data (representation) errors, such as out-of-bound accesses to collections or value overflows and underflows; 
- issues affecting data consistency, frequently due to concurrent accesses, as concurrency is intrinsic to modern software and hardware; 
- issues compromising memory safety, like leaks or unauthorised use; 
- issues related to data use protocols, like forgetting to call mandatory operations or calling operations out of their prescribed order, violating an application's intended behaviour. 

So, many security flaws "are just bugs", and thus, more robust languages and tools for developing software are needed to provide stronger guarantees of application soundness than we have these days. Although society and (inter)national regulation bodies ask for more safety and compliance with laws, the software development industry is, in reality, quite far from being able to deliver safe, secure, and sound products. 

Since most verification methods and tools are very demanding to use, being mastered only by highly trained people, automated techniques tightly coupled with programming development environments are in dire need. A successful approach in the early detection of programming errors is that of types: data type systems are incorporated in most mainstream languages, and flow (aka behavioural) type systems have been developed for many. Behavioural types generalise data types and allow the description of valid sequences of operations, having as a by-product stronger than usual safety guarantees, like deadlock freedom, memory safety, protocol compliance and completion, and thread safety. 

Leveraging on the observation that in Object-Oriented Programming (OOP), it is natural to define stateful objects where the safe use of methods depends on their internal state, we present Java Typestate Checker (JATYC, https://github.com/jdmota/java-typestate-checker), a tool that verifies Java source code with respect to typestates. A typestate defines the object's states, the methods that can be called in each state, and the states resulting from the calls. The tool statically verifies that when a Java program runs: sequences of method calls obey objects' protocols; objects' protocols are completed; null-pointer exceptions are not raised; subclasses' instances respect the protocol of their superclasses. The tool also supports polymorphism with upcasts and downcasts. To the best of our knowledge, this is the first OOP tool that simultaneously tackles all these aspects.

António Ravara is an Associate Professor at the Computer Science Department of the NOVA School of Science and Technology, NOVA University Lisbon (https://www.di.fct.unl.pt/en). Integrated researcher at the NOVA Laboratory for Computer Science and Informatics (https://nova-lincs.di.fct.unl.pt/).
Previously, António was an Assistant Professor at the Department of Mathematics of Técnico (University of Lisbon), where he got an MSc and PhD in Mathematics, specialisation in Theoretical Computer Science.
António's research interests are methods to ensure programs are correct and software systems are reliable and robust, focusing in the foundations of concurrent and distributed systems.

https://novaresearch.unl.pt/en/persons/ant%C3%B3nio-maria-lobo-c%C3%A9sar-alarc%C3%A3o-ravara
https://orcid.org/my-orcid?orcid=0000-0001-8074-0380
https://scholar.google.pt/citations?user=HuxP2pUAAAAJ&hl=en