2 ms·
Honestly? I don't know for sure. On one hand, my understanding is that they used TLA+ to validate the model[0]. One would assume that if they went to that trou
by to11mtm 5y ago
Honestly? I don't know for sure.
On one hand, my understanding is that they used TLA+ to validate the model[0]. One would assume that if they went to that trouble there is at least a specification for how it should work.
OTOH, Specifications can be flawed. This security issue appears unrelated to the design of Cosmos DB itself tho.
[0] - https://en.wikipedia.org/wiki/TLA%2B#Industry_use https://en.wikipedia.org/wiki/TLA%2B#Industry_use
- buitreVirtual 5y agoFor formal verification to catch the bug, the bug would have to be at the design level and the model would have to have enough detail to include the design bug.
- manigandham 5y agoTLA+ is used to design the database itself, including the storage layer, distributed operations, and consensus/consistency models. This bug is a security issues in an entirely separate component. No formal logic is going to warn you about exposed read/write keys.