|
2014-02-18: NSW Big Picture Seminar Franklin (University of
California, Berkeley) on The Berkeley Data Analytics Stack:
Present and Future
|
|
This talk will outline the AMPLab's research approach and
describe how we have integrated the three main resources
available to address the cross-disciplinary nature of Big
Data challenges: Algorithms (such as machine learning and
statistical techniques), Machines (in the form of
scalable clusters and elastic cloud computing), and
People (individually as analysts and as crowds).
|
|
2014-01-16: Seminar Clarke & Osterweil (University of
Massachusetts Amherst) on Process-based Security Analysis
for Human-intensive Systems
|
|
This talk describes a process-model based, systematic
approach for detecting security vulnerabilities in
human-intensive systems. Such systems typically involve
complex interaction and cooperation among software
applications, hardware devices, and human participants,
and are increasingly central to key societal
infrastructure.Thus, protecting such systems from attack
is correspondingly centrally important. Clarke and
Osterweil view is that these systems can be viewed as
collections of processes whose security can be improved
by modelling, analysing, and subsequently using the
feedback gained to support continuous improvement. Their
work features a process-modelling notation, with rich and
well-defined semantics, that is able to represent the
complexity of such systems as well as be the subject of
rigorous analysis, such as model checking and fault-tree
analysis. In this talk, Clarke and Osterweil will
describe how they applied their approach to models of
election processes used in Yolo and Marin Counties in
California, show how their analyses have identified some
example vulnerabilities, and indicate the kinds of
improvements that can reduce vulnerabilities. Although no
system can ever be made immune to any possible attack,
Clarke and Osterweil believe that their approach of using
technology to support continuous improvement represents
an effective way to address the urgent need to protect
the key infrastructure.
|
|
2014-01-01
A paper titled Improved
device driver reliability through hardware verification
reuse has been accepted for publication in the
16th
ASPLOS Conference. The paper is the result of a
collaboration with Intel (Hillsboro, OR) lead by SSRG
researcher Leonid Ryzhyk.
|
|
A further 150K external funding was approved for
AURIN/HTS project to integrate HTS data on the national
map
|
|
2013-12-17: Seminar Bourke (INRIA & ENS - Paris) on
Mechanization of a mesh network routing protocol & the
proof of its loop freedom in Isabelle/HOL
|
|
This talk describes recently completed work to transfer a
formal but pencil-and-paper model and analysis of a
wireless mesh network protocol (AODV) into the proof
assistant Isabelle/HOL. The nodes of such networks are
reactive systems that cooperate to provide a global
service (the sending of messages from node to node)
satisfying certain correctness properties (messages are
never sent in circles).
|
|
2013-12-09: Seminar Khakpour (Royal Institute of Technology
KTH - Stockholm) on Formal Verification of Information Flow
Security for a Simple ARM-Based Separation Kernel
|
|
A separation kernel simulates a distributed environment
using a single physical machine by executing partitions
in isolation and appropriately controlling communication
among them. We present a formal verification of
information security for a simple separation kernel for
ARMv7.
|
