Presentation

file

Visible to the public Digital Engineering Implementation across the Department of Defense.pdf

Digital Engineering is a catalyst for change in engineering methods and tools. In order to fully realize the change, architectures and other formal methods are necessary; and necessary to be understood by the user. This presentation will describe the digital engineering concept, where the DoD is in the change process, and set the stage for discussions on the value to systems development.

file

Visible to the public The Changing Face of Computational Propaganda

There is a growing body of research on the use of social media and other digital communication tools in attempts to manipulate both human and computational systems. But how is computational propaganda, the use of automation and algorithms in online attempts to alter public opinion, changing? How can we best study these changes? This talk explores the rise of AI chatbot, rather than simple social bots, in transnational political information operations. It also discusses two new forms of computational propaganda: "geo-propaganda" and "encrypted-propaganda".

file

Visible to the public Cognitive Security

file

Visible to the public Improving Computer Security by Understanding Cognitive Security

The recording of this talk will only be available to those who registered for the HCSS Conference. If you would like to request access to view this presentation video, please contact hcss@cps-vo.org.

file

Visible to the public The Economics of Cyber Security

file

Visible to the public Distributed and Trustworthy Automated Reasoning

Distributed automated reasoning has become increasingly powerful and popular. This enabled solving very hard problems ranging from determining the correctness of complex systems to answering long-standing open questions in mathematics. The tools are based on a portfolio of solvers that share information or divide-and-conquer. The portfolio approach is effective on large formulas from industry, while divide-and-conquer shines on hard-combinatorial problems. Recently distributed solvers competed for the first time, with each tool running on 1600 cores in the Amazon cloud.

file

Visible to the public KEYNOTE: Take a SEAT: Security-Enhancing Architectural Transformations

System architecture models in a language such as AADL provide a high-level setting in which existing implementations, new design features, high-level requirements, and verifications can be combined. We have recently been developing selected architecture-to-architecture transformations as a way to enhance the security of a system. The transformations are formally specified at a high level and mapped to implementations by a sequence of correctness-preserving (and deductively justified) compilation steps.
file

Visible to the public Trustworthy AI: New Properties for New Complex Systems

Recent years have seen an astounding growth in deployment of AI systems in critical domains such as autonomous vehicles, criminal justice, healthcare, hiring, housing, human resource management, law enforcement, and public safety, where decisions taken by AI agents directly impact human lives. Consequently, there is an increasing concern if these decisions can be trusted to be correct, reliable, fair, and safe, especially under adversarial attacks.
file

Visible to the public Code-Level Model Checking in the Software Development Workflow

This experience report describes a style of applying symbolic model checking developed over the course of four years at Amazon Web Services (AWS). Lessons learned are drawn from proving properties of numerous C-based systems, e.g., custom hypervisors, encryption code, boot loaders, and the FreeRTOS operating system. Using our methodology, we find that we can prove the correctness of industrial low-level C-based systems with reasonable effort and predictability.