SoylentNews is people
SoylentNews
BrakTooth is a collection of flaws affecting commercial Bluetooth stacks on more than 1,400 chipsets used in billions of devices – including smartphones, PCs, toys, internet-of-things (IoT) devices and industrial equipment – that rely on Bluetooth Classic (BT) for communication.
On Thursday, CISA urged manufacturers, vendors and developers to patch or employ workarounds.
The PoC has been made available on the BrakTooth website on GitHub.
As the paper pointed out, all that attackers need to do to pick apart the BrakTooth bugs is an off-the-shelf ESP32 board that can be had for $14.80, (or as low as $4 for an alternative board on AliExpress), custom Link Manager Protocol (LMP) firmware, and a computer to run the PoC tool.
Researchers from the University of Singapore disclosed the initial group of 16 vulnerabilities (now up to 22), collectively dubbed BrakTooth, in a paper published in September. They found the bugs in the closed commercial BT stack used by 1,400+ embedded chip components and detailed a host of attack types they can cause: Mainly denial of service (DoS) via firmware crashes (the term “brak” is actually Norwegian for “crash”). One of the bugs can also lead to arbitrary code execution (ACE).
Since the paper was published, there have been a number of updates, as vendors have scrambled to patch or to figure out whether or not they will in fact patch, and as researchers have uncovered additional vulnerable devices.
(Score: 2, Insightful) by shrewdsheep on Monday November 08 2021, @08:00AM
You should be aware that formal methods do not add anything to the development cycle. The fundamental question is whether a program is "correct" (which is hard to define in itself). You can start writing pages of proofs but this will not improve the code nor will it ever proof that the code is correct as the correctness of the proof has to be proved (i.e. an infinite regression). Just consider the function that adds one to an integer. If you start to proof that your implementation is correct you can only obscure your solution. I believe that this is the reason why formal methods have stayed irrelevant ever since their invention (well, I heard that NASA formally developed the code for the Apollo missions).
Code should be as clearly written as to serve as a proof by and in itself. Together with clear APIs, programs can then be understood and modified. This is complemented with unit testing. As a matter of fact, in mathematically logic the truth of a statement can be shown by checking all values of the free variables. Unlike formal proofs, this step can be completely formalized in software which is why it was more successful IMO.