source:  sent by Rob Wiltbank, Galois

Our friends at GALOIS (thanks to Artemus FAN, Rob Wiltbank!) have been gracious in allowing us to post their take on the recent 'KRACK" (WPA2) vulnerability.  We reported the vulnerability in our last issue of "Artemus Spotlights".  Take a look at that posting here.


On Monday, October 16, the KRACK vulnerability to WPA2 was revealed in a paper by Mathy Vanhoef and Frank Piessens. KRACK enables a range of attacks against the protocol, resulting in a total loss of the privacy that the protocol attempts to guarantee. For more technical details on the attack, the website and the Key Reinstallation Attacks (KRA) paper are the best place to look. The paper presents the problem clearly, and you will learn about a protocol that you use constantly. Furthermore, it presents a number of compelling attacks that show exactly how big of a problem KRACK is. This post will discuss what the KRACK paper has to teach us about formal methods and cryptography standards.

It’s a little surprising that a protocol as widely used as WPA2 still harbors critical vulnerabilities. Even more surprising is that portions of the protocol have been formally verified (mathematically proved) to be secure! Why don’t these factors guarantee that the protocol is free of such critical vulnerabilities? The KRA paper raises the following concerns about standards and formal verification. These provide us with valuable insight into pitfalls to avoid as we perform and present our work:

  1. Specifications for a protocol may not be precise enough to guarantee security.
  2. Real-world implementations may not match formal specifications used in proofs.
  3. Formal proofs might lead to complacency, discouraging future audits and inspections.

At Galois, we believe strongly in the value of formal verification, so we think it’s worth examining each of these points. In doing so, we gain some insights into real-world cryptography verification.

Concern: Specifications may not be precise enough

It is impossible to test for security. Security is a property of all possible behaviors of a system, so the time to get security right is when the system is defined. KRACK is a vulnerability in the specification of the WPA2 protocol, and it is exacerbated in some cases by decisions that implementors made in the face of an ambiguous specification. Any of these decisions allow the implementations to function correctly. After all, we’ve been successfully utilizing WPA2 for a long time without noticing any significant functionality shortcomings. In the face of the KRACK vulnerability, however, these ambiguities allow for significantly more damaging attacks.

We can ensure that specifications are unambiguous by making them more formal. Often, ambiguity hides in natural language specifications in ways that are difficult to understand until the specifications are represented formally. A formal specification serves as an intermediate point between the easily ingestible natural language specifications we typically see today and the more complicated implementations.


A look back at WannaCry, NotPetya, Locky, and other destructive ransomware campaigns to infect the world this year.


Who needs a horror movie when you have the 2017 ransomware news cycle? There has been a constant stream of increasingly destructive attacks hitting victims around the world.

Ransomware attacks are getting easier to launch as well. New research from Trustwave shows ransomware is now being distributed through an exploit for Microsoft Dynamic Data Exchange (DDE). Attackers can use Word and Outlook to execute malicious code with DDEAUTO, which allows for automatic code execution that can be abused by threat actors.

Major threat actors have started to toy with this exploit and use the Necurs botnet to distribute massive attacks on email gateways. The Necurs email campaign has an attached Open Office Word document with the malicious DDE exploit code. This code executes a PowerShell script, which downloads another script, which eventually downloads a Locky ransomware file.

The ease of this type of attack, complexity of defending against it, and number of applications infected means the DDE exploit will continue to be used among attackers, Trustwave researchers predict, and more in the near future.

When it comes to ransomware campaigns, "this past year was unlike anything we've ever seen," said David Dufour, vice president of engineering and cybersecurity at Webroot, which recently compiled the most destructive ransomware campaigns to hit so this year.

Locky is one of the nastiest attacks to hit in 2017. What are the others? Let's take a look back:

NotPetyaIn June 2017, a fake Ukrainian tax software update spread laterally through infected networks like a worm, using attack vectors Supply Chain ME.doc and the EternalBlue and EternalRomance exploits. NotPetya, a variant of the older Petya attack, charged $300 in ransom from victims in 100+ countries.

WannaCryThe first ransomware to spread via Server Message Block (SMB) exploit was created in March 2017 and attacked in May 2017. WannaCry used the EternalBlue SMB Exploit Kit to infect more than 200,000 machines on day one. Victims spanning 150+ countries were charged $300-$600 in ransom.

LockyIt first appeared in 2016 but continues to be a threat in 2017, with 28+ countries hit in total. Locky arrives as a fake shipping invoice spam email which, once opened, downloads malware and encryption components. Ransom ranges between $400-$800.

Jaff: This May 2017 campaign also hit victims with phishing emails. Like Locky, it contains traits related to other forms of malware. It has demanded $3,700 in ransom from victims in 21+ countries.


Honeywell teased an upcoming security system in mid-October. The thermostat giant Wednesday shared more details about its US-only Smart Home Security System. Available starting Wednesday through Indiegogo, the do-it-yourself kit will make its way to retail in early 2018.

Here's the gist. The Smart Home Security System is a scalable (and largely indoor) DIY home security system. The Camera Base Station acts as the system's central hub. It's outfitted with 1080p high-definition livestreaming, a 145-degree viewing angle and free 24-hour cloud storage (this will jump up to three days during a future update).

The system also comes with a variety of optional accessories, including door and window sensors, key fobs, motion sensors and indoor or outdoor MotionViewers -- cameras with integrated motion sensors.

Here's a list of the products available with the system and their retail prices:

Starter Kit (Camera Base Station, 2 Access Sensors, Key Fob) -- $500
Camera Base Station -- $400
Door and Window Access Sensors -- $40
Key Fob -- $30
Motion Sensor -- $50
Indoor MotionViewer -- $80
Outdoor MotionViewer -- $170

Note: Honeywell says Indiegogo backers will get a discount through Dec. 16, but haven't yet shared how much.

Honeywell is just one of a number of companies introducing DIY home security systems. NestRingWink and SmartThings have all announced new systems within the last two months. At $500, Honeywell's Starter Kit is priced to compete with the $499 Nest Secure alarm system and the $550 SmartThings Starter Kit. Both the Ring and the Wink starter kits cost $199.


Anyone who remembers the Mirai botnet, used to cause widespread internet outages in 2016, might have been forgiven for thinking progress had been made to prevent a similar disaster. But a mysterious botnet, dubbed the "IoT Reaper," has ballooned in recent days by taking advantage of the same vulnerable, internet-connected cameras as Mirai did. And as cybersecurity experts warn the Reaper could be a bigger threat than its forbears, Forbes has seen firsthand how hacking a CCTV camera can be used not just for web destruction, but Ocean's 11-style machinations.

In a demonstration hack, Leigh-Anne Galloway, cybersecurity resilience lead at Positive Technologies, abused a flaw in cameras containing code from Chinese manufacturer Dahua. That company's software can be found, and possibly tampered with, in just over 400,000 devices, as shown on the IoT search engine Shodan. In seconds, Galloway's exploit allowed her to quickly switch out the real feed for another. It's not hard to imagine high-tech heists being made significantly easier with such a quick and dirty hack of a CCTV camera.

While the vulnerability was patched with a firmware update back in July, and the US Computer Emergency Response Team put out an alert, Galloway doesn't think many would have updated, as was the case with Mirai.