Getting the measure of cybercrime?

Cybercrime is now a well-established and widely recognised concern, with criminal behaviour probably representing the main driver behind the huge increase in numbers of malicious programs over the last decade or so.  However, while there is no doubt that the problem exists, attempts to quantify cybercrime have resulted in dramatically varied numbers, highlighting the difficulty of trying to establish the scale, cost and impact of attacks.

In this presentation, Steven Furnell examines the nature (and potential quality) of the measures currently used to quantify cyber-dependent crime.  He then proceeds to consider the opinions of various security practitioners regarding the potential disconnect between such measurements and the aspects that are potentially more important for us to understand.  The discussion draws upon work conducted as part of a recent Home Office-funded study into the scale, trends and measurement of cyber-dependent crimes.

Cyber Threat Intelligence might not be the solution

Cyber Threat Intelligence (CTI) is perceived as the next big “thing” that can help reduce, slow down or stop the increasing number of cyber-attacks.  However, CTI means different things to different people. Should that really be the case? Despite the proliferation and the cost of threat intelligence feeds, the threat level remains high in most cases i.e. mitigations against cyber-attacks are not as effective as they could be.

The question is: What are the requirements for efficient cyber threat intelligence? How we can assess its success will be explored during this seminar. We will close by discussing some of the author’s work on the topic.

The Quest for Assured Confidentiality

Speaker: Toby Murray (NICTA)

 

Abstract: Protecting the confidentiality of sensitive information has been a goal of secure operating systems kernels for the last 30 years. However, monolithic kernels are routinely exploited and even smaller kernels and hypervisors cannot guarantee the absence of storage and timing channels.

 

The seL4 kernel was famously the world’s first general-purpose kernel to have its C code implementation proved functionally correct. In this talk, we describe the ongoing quest to assure that seL4 can enforce strong confidentiality against untrustworthy programs, using both formal and empirical approaches.

 

The first step on this journey was a proof of intransitive noninterference for the seL4 implementation, which ensures confidentiality up to (1) potential storage channels in parts of the instruction set architecture (ISA) unused by seL4 and (2) timing channels. We then tackled ISA storage channels by additional proofs over a trustworthy formal model of the ARMv6 ISA. These confirmed a potential channel, since corrected, undetected by the noninterference proof.

 

However, timing channels remain beyond the reach of formal proof.

 

Therefore, we recently performed a thorough empirical analysis of the effectiveness of some well-known timing channel countermeasures implemented in seL4. The results revealed that the effectiveness of each countermeasure is highly platform dependent, confirming the value of the empirical approach. Taken together, this body of work is the most comprehensive collection of evidence yet assembled on the ability of a general-purpose kernel to enforce confidentiality.

 

Bio: Toby Murray is a Senior Researcher at NICTA and a Conjoint Lecturer in the School of Computer Science and Engineering at the University of New South Wales. His research focuses on the use of formal verification to build and assure highly secure systems. His current work is centred around building and assuring high security systems on the seL4 microkernel, as well as developing proof-producing domain specific languages (DSLs) for writing verified systems software at minimal cost.

 

Toby previously led NICTA’s Information Flow project which completed the world’s first proof of intransitive noninterference for a general-purpose kernel, seL4, building on seL4’s earlier landmark functional correctness verification.

 

Before joining NICTA, Toby obtained his D.Phil. from the University of Oxford in 2010. His thesis applied the process algebra CSP to analyse the security of reusable capability-based software abstractions, and was supervised by Gavin Lowe. Before that he worked for the Defence Science and Technology Organisation researching and developing next generation secure pervasive computing technology as part of the Annex project.

https://www.cs.ox.ac.uk/seminars/1303.html