This paper presents a methodology for generating formally proven equivalence theorems between decompiled x86-64 machine code and big step semantics. These proofs are built on top of two additional contributions. First, a robust and tested formal x86-64 machine model containing small step semantics for 1625 instructions. Second, a decompilation-into-logic methodology supporting both x86-64 assembly and machine code at large scale. This work enables black-box binary verification, i.e., formal verification of a binary where source code is unavailable. As such, it can be applied to safety-critical systems that consist of legacy components, or components whose source code is unavailable due to proprietary reasons. The methodology minimizes the trusted code base by leveraging machine-learned semantics to build a formal machine model. We apply the methodology to several case studies, including binaries that heavily rely on the SSE2 floating-point instruction set, and binaries that are obtained by compiling code that is obtained by inlining assembly into C code.
Tag: Intel
6 Intel security advisories
INTEL-SA-00212
Intel® System Support Utility for Windows Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00212.html
INTEL-SA-00207
Intel® SSD Data Center Tool Vulnerability Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00207.html
INTEL-SA-00203
Intel® SGX Platform Software and Intel® SGX SDK Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00203.html
INTEL-SA-00182
Intel® PROSet/Wireless WiFi Software Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00182.html
INTEL-SA-00175
Intel® Optane™ SSD DC P4800X Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00175.html
INTEL-SA-00144
Intel® NUC Firmware Security Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00144.html
Project Celadon: Trusty Hardware Binding Developer Guide is now available
Roger Feng announced the availability of a new document for Project Celadon, the Intel-specific version of Android.
The Trusty Hardware Binding Developer Guide is now available at 01.org:
https://01.org/projectceladon/documentation/tutorials/trusty-hardware-binding
Alternatives for SMM usage in Intel Platforms
2019 OCP Global Summit:
Case Study: Alternatives for SMM usage in Intel Platforms
Sarathy Jayakumar, Principal Engineer – Firmware, Intel Corporation
The broadcast System Management Mode (SMM) model has been used for many years to manage priority system events but has a number of disadvantages. Overuse of System Management Interrupts (SMI) results in performance degradation, increases latency with higher core counts, and introduces potential race conditions. SMM is also difficult to debug and has access to system resources outside of the OS environment, which makes it target for firmware exploits. This session expands on Intel’s initiative to reduce SMM footprint and provide alternatives for handling runtime platform events. Intel described SMI reduction methods based on Protected Runtime Mechanism (PRM), UEFI Capsule, and the Baseboard Management Controller (BMC) at the 2018 OCP Regional Summit. The presentation features a case study and demonstration using Intel® Xeon® Scalable Processors with EDK II firmware.
https://www.opencompute.org/summit/global-summit
Intel: An update on SGX 3rd Party Attestation
INTEL-SA-00131: Intel Power Management Controller (PMC) EoP
Power Management Controller (PMC) Security Advisory
Intel ID: INTEL-SA-00131
Advisory Category: Firmware
Impact of vulnerability: Escalation of Privilege, Information Disclosure
Severity rating: HIGH
Original release: 09/11/2018
Last revised: 12/18/2018
A potential security vulnerability in power management controller firmware may allow escalation of privilege and/ or information disclosure. Intel is releasing firmware updates to mitigate this potential vulnerability.
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00131.html
Intel to open-source FSP??
https://www.phoronix.com/scan.php?page=news_item&px=Intel-Open-Source-FSP-Likely
Please leave a Comment on this post if you have more info, other than above.
Intel releases 5 new security advisories
Intel® QuickAssist Technology for Linux Advisory
INTEL-SA-00211
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00211.html
Intel® System Defense Utility Vulnerability Advisory
INTEL-SA-00209
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00209.html
Intel® Parallel Studio Vulnerability Advisory
INTEL-SA-00208
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00208.html
Intel® Solid State Drive Toolbox File Permissions Advisory
INTEL-SA-00205
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00205.html
Intel® VTune Amplifier 2018 Update 3 Advisoy
INTEL-SA-00194
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00194.html
CVE-2018-12155, INTEL-SA-00202: Intel Integrated Performance Primitives advisory
Advisory Category: Software
Impact of vulnerability: Information Disclosure
Severity rating: MEDIUM
Original release: 12/05/2018
A potential security vulnerability in Intel® IPP may allow information disclosure. Intel is releasing software updates to mitigate this potential vulnerability. Data leakage in cryptographic libraries for Intel(R) IPP before 2019 update1 release may allow an authenticated user to potentially enable information disclosure via local access. Intel recommends that users of Intel® IPP update to 2019 update1 or later. Updates are available for download […] Intel would like to thank an Wichelmann (Universität zu Lübeck), Ahmad Moghimi (Worcester Polytechnic Institute), Thomas Eisenbarth (Universität zu Lübeck) and Berk Sunar (Worcester Polytechnic Institute) for reporting this issue and working with us on coordinated disclosure.
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00202.html
https://cve.mitre.org/cgi-bin/cvename.cgi?name=2018-12155
MinnowBoard Max/Turbot firmware 1.00 released
SUPPORTED (NEW) FEATURES AND CHANGES IN RELEASE:
1. The 64bit BIOS is now functional with Linux and Windows 8.1 Embedded/Windows 10.
2. The 32bit BIOS is now functional with Windows 8.1 Embedded/Windows 10.
3. Supports booting from "SD card", "USB drive" and "SATA".
4. Supports S3 resume for Linux, Windows 8.1 Embedded and Windows 10.
5. Supports S4 resume for Windows 8.1 Embedded and Windows 10.
6. Supports 64bit image GCC build (32bit image GCC build is not supported).
7. Update EDK II core from UDK2015 release to UDK2017.
8. Signed Capsule Update is supported.
9. Supports HTTP and HTTPS boot.
10. Add board UUID support.
11. Fixed the issue that USB device may not be detected at system power-on.
12. Main changes in this release
1) Add microcode M0130679906 for D1 stepping.
2) Produce SMBIOS type 1.
3) Changed manufacture name.
4) Fixed some open bugs. Please visit the following link for details.
https://wiki.yoctoproject.org/wiki/Minnow_Bug_Triage
https://firmware.intel.com/projects/minnowboard-max
https://firmware.intel.com/sites/default/files/minnowboard_max-rel_1_00-releasenotes.txt
CHIPSEC v1.3.6 released
New or Updated Modules:
Updated memconfig to only check registers that are defined by the platform
Updated common.bios_smi to check controls not registers
Added me_mfg_mode module
Added support for LoJax detection
Updated common.spi_lock test support
Added sgx_check module and register definitions
Updates to DCI support in debugenabled module
New or Updated Functionality:
Added ability for is_supported to signal a module is not applicable
Added 300 Series PCH support
Added support for building Windows driver with VS2017
Added fixed I/O bar support
Updated XML and JSON log rewrite
Updated logger to use python logging support
Added JEDEC ID command
Added DAL helper support
Added 8th Generation Core Processor support
Updated UEFI variable fuzzing code
Added C600 and C610 configuration
Added C620 PCH configuration
Updated ACPI table parsing support
Updated UEFI system table support
Added Denverton (DNV) support
Added result delta functionality
Added ability to override PCH from detected version
See release notes for list of Fixes.
Intel security guidance: Host Firmware Speculative Execution Side Channel Mitigation
[…]This provides specific guidance for firmware based upon the EFI Developer Kit II (EDKII) and coreboot. Because this document deals with host firmware internal requirements, it is not intended to provide side channel mitigation guidance for general application developers.
Scope: This addresses bare-metal firmware runtime risks and mitigation suggestions for the bounds check bypass, branch target injection, rogue data cache load, rogue system register read, and speculative store bypass side channel methods. Our examples and context are primarily focused on ring 0 firmware runtimes (for example: EFI Developer Kit II, PI SMM, and coreboot SMM). Other firmware execution environments are out of scope.[…]
more info:
https://software.intel.com/security-software-guidance/software-guidance
Intel ‘patch Tuesday’: 8 new security advisories
INTEL-SA-00199
Intel® RAID Web Console 3 Cross-site Scripting Vulnerability Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00199.html
INTEL-SA-00198
Intel® Ready Mode Technology File Permissions Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00198.html
INTEL-SA-00197
Intel® Media Server Studio for Windows® Vulnerability Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00197.html
INTEL-SA-00196
Intel® RAID Web Console 3 for Windows Authentication Bypass Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00196.html
INTEL-SA-00188
Intel® PROSet/Wireless WiFi Software Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00188.html
INTEL-SA-00187
Intel® Driver & Support Assistant Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00187.html
INTEL-SA-00180
Intel® Trace Analyzer 2018 Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00180.html
INTEL-SA-00153
Intel® Rapid Store Technology Installer Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00153.html
Intel: Protection at the Hardware Level [using SGX]
Intel has a new document about hardware security and SGX:
There is tremendous opportunity for application and solution developers to take charge of their data security using new hardware-based controls for cloud and enterprise environments. Intel® Software Guard Extensions (Intel® SGX), available in its second-generation on the new Intel® Xeon® E-2100 processor, offers hardware-based memory encryption that isolates specific application code and data in memory. Intel® SGX allows user-level code to allocate private regions of memory, called enclaves, which are designed to be protected from processes running at higher privilege levels. We believe only Intel offers such a granular level of control and protection. Think about it like a lockbox in your home. Even though you have locks on your doors and a home security system, you may still secure your most sensitive data in a private lockbox with a separate key to provide extra layers of protection even if someone gained unwanted access to your home. Essentially, Intel® SGX is a lockbox inside a system’s memory, helping protect the data while it’s in-use during runtime.[…]
upos.info: Latency, Throughput, and Port Usage Information For Instructions on Recent Intel Microarchitectures
This website provides more than 200,000 pages with detailed latency, throughput, and port usage data for most x86 instructions on all generations of Intel’s Core architecture (i.e., from Nehalem to Coffee Lake). While such data is important for understanding, predicting, and optimizing the performance of software running on these microarchitectures, most of it is not documented in Intel’s official processor manuals.
ZeroNights 2018: NUClear explotion
Alexander Ermolov and Ruslan Zakirov will deliver their «NUClear explotion» talk. A major and most significant approach to UEFI BIOS security is preventing it from being illegitimately modified and the SPI flash memory from being overwritten. Modern vendors use a wide range of security mechanisms to ensure that (SMM BLE / SMM BWP / PRx / Intel BIOS Guard) and hardware-supported verification technologies (Intel Boot Guard). In other words, they do everything just not to let an attacker to place a rootkit into a system. Even the likelihood of execution in the most privileged mode of a processor – System Management Mode (can be achieved through vulnerable software SMI handlers) – is of no interest to adversaries since it does not guarantee they will be able to gain a foothold in a system. A single reboot and an attack must be started anew. However, there is a thing that can make all BIOS security mechanisms inefficient. And this thing is a vulnerable update mechanism implemented by a vendor. Moreover, quite often a legitimate updater adds lots and lots of critical security holes to a system. In this talk, we will speak about how vendors manage to throw all those security flaws together in one system using Intel NUC, a small home PC, as an example. Besides, we will demonstrate how an adversary can compromise BIOS from the userland.
https://2018.zeronights.ru/en/news/the-selection-of-zeronights-2018-talks-is-finished/
Telemetry: Enhancing Customer Triage of Intel® SSDs
by Behnam Eliyahu and Monika Sane
Telemetry refers to an umbrella of tools, utilities, and protocols to remotely extract and decode information for debugging potential issues with Intel® SSDs. Telemetry works over industry standard protocols, and eliminates or minimizes the need to remove SSDs from customer systems for retrieving debug logs. Telemetry thus enables host tools, Intel technical sales specialists, (TSS), Intel application engineers (AEs), and Intel engineering teams to better identify and debug performance excursions, exception events and critical failures in Intel® SSDs, without sending the physical drive to Intel for failure analysis. This capability is designed in accordance with NVMe* 1.3 telemetry specifications as well as corresponding ACS 4 SATA definitions (which are common industry standards), and is expected to accelerate debugging of external and internal bug sightings pertaining to Intel® SSDs. The key difference between NVMe and SATA is the fact that there is no controller-initiated capability on SATA drives.[…]
https://itpeernetwork.intel.com/telemetry-enhancing-customer-triage/
See-also:
https://github.com/linux-nvme/nvme-cli/blob/master/Documentation/nvme-telemetry-log.txt
https://github.com/linux-nvme/nvme-cli/blob/master/linux/nvme.h
https://jmetz.com/2018/02/whats-new-in-nvme-1-3/
https://nvmexpress.org/resources/specifications/
Intel seeks Security Researcher
Responsible for secure design, development and operation of Intel’s hardware and software products and services. Responsibilities may include threat assessments, design of security components, and vulnerability assessment.
4+ years of experience in the field of system security research and exploring software and hardware techniques as a method of attack against targets within compute systems.
In-depth experience with security threats, vulnerability research, physical attack techniques (power analysis, fault injection, reverse engineering, etc.), side-channel attack methods.
Knowledge of security technologies: authentication, cryptography, secure protocol, etc.
Knowledge of computer architecture CPU, SoC, chipsets, BIOS, Firmware, Drivers, and others
https://jobs.intel.com/ShowJob/Id/1826346/Security%20Researcher
How Does an Intel Processor Boot?
When we switch on a computer, it goes through a series of steps before it is able to load the operating system. In this post we will see how a typical x86 processor boots. This is a very complex and involved process. We will only present a basic overall structure. Also what path is actually taken by the processor to reach a state where it can load an OS, is dependent on boot firmware. We will follow example of coreboot, an open source boot firmware.[…]
https://binarydebt.wordpress.com/2018/10/06/how-does-an-x86-processor-boot/
6 new security advisories from Intel
Intel® Server Boards Firmware Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00179.html
Intel® RAID Web Server 3 Service Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00171.html
Intel® NUC Bios Updater Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00168.html
Intel® NVMe and Intel® RSTe Driver Pack Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00166.html
Intel® Server Board Firmware Advisory
https://www.intel.com/content/www/us/en/security-center/advisory/intel-sa-00138.html
