Alexis Duque PhD student at the CITI Lab, INSA Lyon - Agora Team, INRIA.

SSTIC Part 2

This post is the second part of my notes I took during the SSTIC this year. The first part is available here: SSTIC 2018 Part 1

RUMP : Nordic made easy

Salma El Mohib

Speaker from Digital Security presents 3 python scripts for nRF firmware analysis. Problem: How to reverse a nRF firmware with IDA? How to map it in IDA?

In fact, the nRF soft device use SVCALLS.

  • nrfparse.py: build the knowledge database from all the Nordic SDK and softdevice
  • nrfident.py: nRF device identification + SDK and Soft Device version to get the memory mapping
  • nrfreverse.py: used after IDA configuration and firmware disassembly. It parses the assembly code to find SVC opcodes. It selects the appropriate functions prototypes and outputs them in the python output window of IDA pro.

The tool is available on Github: nrf5x-tools

RUMP: ARM_Now

Sanson Chaignon

ARM_Now is a qemu powered tool that allows instant setup of virtual machines on arm CPU, mips, powerpc, nios2, x86 and more, for reverse, exploit, fuzzing and programming purpose.

ARM_Now is available on Github: arm_now

Audit de sécurité d’un environnement Docker

Julien Raeis, Matthieu Buffet (ANSSI)

Docker is a lightweight virtualization tool for packaging applications and automating the dev/deployment cycle. Each application block is a container. Each container has all the files it depends on. Docker works under windows & Linux. For a developer, docker images are black boxes in which the application runs. They often do not master the security of their software execution environment. On the security side, this presentation will focus on the part that makes the Docker images turn and how to harden the host environment.

Windows Docker containers are based on JOBS kernel objects that provide a CGROUP equivalent on Linux. We can look at the container tree using winobj. Each container is in a silo, and in these silos, we discover the isolation mechanism for the symbolic links to be executed in a separate context. On the filesystem side, the NTFS driver has been patched to handle the isolation. If it is available, Docker uses Hyper-V to isolate the container and benefits from the Hyper-V isolation mechanism.

For the audit of a Docker environment, we can control the network interfaces, the permissions on the docker group, mutual authentication by certificates, etc … If we do not do it, we expose ourselves to an escalation of privileges via Docker. To avoid denials of service, we often limit the consumption of resources via ulimit.

Namespaces should be reviewed, especially those that allow to make IPC, to do ptrace, etc.

To facilitate the auditing of namespaces, speakers have developed a tool to generate a graph according to which namespace can access which process.

Process capabilities can be reduced using the tool pscap. Then we can use the docker commands to reduce these capabilities. When the container has access to real-world resources on the Host, it must be ensured that these resources do not allow elevation of privilege to the Host.

Windows Server Containers are not secure and do not isolate the executed code of the Host. We must therefore favor Hyper-V Containers, rather than Windows Server Container.

Under Linux, a seccomp filter is compiled, so if we must decompile it if we want to audit it.

Speakers worked on a formal Prolog verifier that takes a seccomp filter as input and evaluates whether or not specific actions can be performed with this filter.

To improve the containers isolation, it is possible to use Orchestrators based on virtualization, KAtacontainers that offer an equivalent of Hyper-V Containers under windows, gVisor which is a userland kernel made by Google.

Link to the presentaiton

Hardening a Java Card Virtual Machine Implementation with the MPU

Guillaume Bouffard, Léo Gaspard

The speaker will introduce how to make a JavaCard JVM hardened using the features of a CPU. To obtain a trusted root, you need a secure and robust component in which you can store a cryptographic secret that will cryptographically sign and verify the integrity of some parts (or all) of the trusted system.

JavaCard technology is based on the JVM that runs on a smart card. There is no open-source implementation, but the majority of JavaCard platforms are evaluated.

The JVM is often independent of the secure component on which it operates, and the confinement is done at the application level, which at a cost in performance. As a result, the speakers decided to work on this JVM to use the hardware mechanisms of the smart card. The Memory Protection Unit is configured in privileged mode and allows setting the read/write/execution restrictions. But these configurations are limited to 8 memory regions, roughly 8 pages of MMU on a conventional CPU. One region can be included in another to refine the insulation.

Link

Dans les coulisses de l’équipe sécurité Debian

Yves-Alexis Perez

The speaker is a volunteer with the Debian security team. He will introduce his role in the team and how Debian manages the vulnerabilities.

Only 10 peoples, 5 active, all are volunteers. Some other guys help: package maintainers, researchers, project maintainers.

The team job is to manage the distribution security on stable version (Stretch and Jessy). They prepare packages security updates and write security-announce. They coordinate with the other teams: developers, etc.

The Debian security team also contributes to hardening the Debian ecosystem. However, they do not work on the platform security (Debian account and keys management, CI, Debian LTS, etc)

They admin the security tracker website that reports the current distribution security state and publish CVE list.

The security-tracker is a public git repo. They have private repositories, for instance for threats under embargo.

They also monitor external mailing lists, and their mail address about vulnerability reports. To help them in this task, they have the External-check tool that is a script that grabs the CVE and adds them to a list. The list is curated by the team;

  1. the vulnerability is identified
  2. the CVE is assigned
  3. a fix is identified
  4. the patch is applied
  5. the package is built locally
  6. the package is uploaded to security-master
  7. the package is built by the build bots
  8. the package is released to the security mirror
  9. security-announce mail is sent

Different kind of vulnerabilities: public, private and complexes

In practice, embargo delay the patch and not developed by many people

Finally, the speaker introduces some example of vulnerabilities.

KRACK In August, the CERT contact Debian and share all the details, the draft of the paper, and proofs of concept. In October, wpa_supplicant maintainers contact Debian with their current work and patch proposals. To conclude, during the embargo, Debian can learn about the vulnerabilities and check that wpa_supplicant patches are working. At the end of the embargo in November, Debian published the update.

Meltdown: very painful for Debian because it was aware of the vulnerability during the embargo period. Debian got the info about Meltdown the same day as the public. So they can’t get prepared.

Link to the presentation

A Practical Guide to Differential Power Analysis of USIM Cards

Adrian Thillard, Christophe Devine, Manuel San Pedro (ANSSI)

The speaker begins introducing Milenage, an algorithm used to derivate the credentials in SIM cards. Thanks to Milenage, the phone can authenticate itself on the operator network. If an attacker can get secrets from the SIM card, the impact on privacy is huge for the user. To do this, we can perform a power consumption variations analysis using an oscilloscope, also known as DPA. This allows an attacker to identify the execution steps of the algorithm. from traces of references that are not always very clean because the clock of the card is not super precise. We must then re-align the peaks in order to have a proper basis of comparison. On the assumption that the data affects consumption. It requires about 4000 of traces to validate the hypothesis using a 400€ oscilloscope and python scripts. The number of traces required can be reduced using better equipment (e.g a 15000€ oscilloscope).

Link to the presentation

HACL* une bibliothèque de cryptographie formellement vérifiée dans Firefox

Benjamin Beurdouche, Jean Karim Zinzindohoue

The speaker was a member of the INRIA PROCECO team. He will introduce HACL*, a formally verified crypto library. Writing crypto is not really easy. As example, we can have a look at the OpenSSL CVE list: side channel attack, buffer overflow… It is also true for NaCl (salt) which is a modern primitive cryptographic library.

How to improve the situation. How can the community help? Using formal methods. Which approach to choose. 3 axes already exit:

  • using assembly: best performances, no compiler (no bug, no fault introduced), best control on a side channel, ut - specific to the platform
  • using C: portable, good performance, but introduce a compiler
  • using a high-level programming language: easy, but slow,

Thus they propose HACL (hacl-star) : a library with a small size, but complete, autonomous, written in F, C code generated from F code, C code is published

F* is a verification oriented language close to OCaml for proof automation. How to produce C code from F? F -> Low* with F* compiler. Then KreMLin: Low* -> C (correction proof)

What is proved: memory safety, execution independency Safety memory thanks to F*. IF it compiles, the code is safe from the memory point of view.

How to prove the code is correct?

HACL* is faster than C implementation.

Link