kobebrookskC3

8 ms·

61.
by kobebrookskC3 5y ago
do you know if anyone has used frama-c to verify properties as "deep" as those done by seL4, like functional correctness and integrity, rather than a "shallower" property like memory safety or absence of crashes?
62.
by kobebrookskC3 5y ago
of course, with unverified code, "completed" means absence of evidence of bugs, not evidence of absence.
63.
by kobebrookskC3 5y ago
if ur fine with writing 4 lines of code a day from an expert...i guess
64.
by kobebrookskC3 5y ago
afaik, the c is handwritten for performance reasons, and is manually proven to be a refinement of the executable haskell model. the haskell is then proven to be a refinement of an abstract, more succinct spec.
65.
by kobebrookskC3 5y ago
unfortunately, it's unsound https://github.com/mcoblenz/Bronze/issues/2
66.
by kobebrookskC3 5y ago
how about an actual computer services shop as a front?
67.
by kobebrookskC3 5y ago
the worst part is that testing might give something that is reliable against non-malicious inputs, and then explode given malicious ones. actually, that's not the worst part. the worst part is when nothing seems to occur on a malicious
68.
by kobebrookskC3 5y ago
i eagerly await the day when chrome realizes their current situation of being written in a memory unsafe language is untenable. it seems like they're still in denial, but they're slowly realizing https://docs.google.com
69.
by kobebrookskC3 5y ago
is that saying anything if microsoft is basically eternal? what, you think the company that makes excel and windows is gonna go out of business any time soon?
70.
by kobebrookskC3 5y ago
if there was a production-grade memory-safe language with similar performance, i would also advocate for it. it's less that rust is good, and that memory unsafety is bad.
71.
by kobebrookskC3 5y ago
let's check out https://googleprojectzero.blogspot.com/2021/12/a-deep-dive-i... , which has probably been used to enable "crimes against humanity". integer overflow results in undersized allocation w
72.
by kobebrookskC3 5y ago
it's more like being written in a memory-unsafe language is an anti-feature.
73.
by kobebrookskC3 5y ago
the trade-offs are probably made to maximize profits for shareholders, and security is deprioritized as a negative externality.
74.
by kobebrookskC3 5y ago
no, just clarifying the difference between not encountering bugs and not having them.
75.
by kobebrookskC3 5y ago
is your code as actively attacked as a web browser or iOS?
76.
by kobebrookskC3 5y ago
> I have spent strictly more time in the last five years filing compiler bugs than chasing memory usage errors in my C++ code. maybe because your code isn't worth having people actively attack?
77.
by kobebrookskC3 5y ago
i wouldn't mind C if every program written in it was written to the standard of seL4, but alas, that isn't the case, and usually it's not even close. i'm also quite sure that getting even close to it would make you want
78.
by kobebrookskC3 5y ago
why is the "payment processing" software written in c/c++ and not something like java in the first place? i would imagine not needing to care too much about memory would speed up development velocity. was it before java becam
79.
by kobebrookskC3 5y ago
a product can be valuable without being worth attacking, like something that only runs on trusted inputs. the bar for software "worth attacking" for me is that there are people who are paid mainly to find exploits on it, and not j
80.
by kobebrookskC3 5y ago
your code probably isn't worth attacking
81.
by kobebrookskC3 5y ago
idk, many large companies report about 70% of their security issues are due to memory unsafety. reducing your security bugs by a factor of 3 sounds pretty compelling to me...
82.
by kobebrookskC3 5y ago
when "human error" happens at a much higher rate than the alternatives, it's fair to blame it.
83.
by kobebrookskC3 5y ago
pretty sure the people who wrote the vulnerable code were experts.
84.
by kobebrookskC3 5y ago
feel free to keep writing c, as long as you prove all your code memory safe. i'm gonna take a stab and say writing rust is easier.
85.
by kobebrookskC3 5y ago
> Rust is trying to solve problems we don't have. I'm sure you mean negative externalities that your customers aren't equipped to appropriately price.
86.
by kobebrookskC3 5y ago
what does zig offer over c/c++ with sanitizers?
87.
DARPA Drone Cybersecurity Software Foils Hackers in Demo(airforcemag.com)
3 points by kobebrookskC3 5y ago|0 comments
88.
by kobebrookskC3 5y ago
hey, whaddya know, i just stumbled upon this today https://twitter.com/geofft/status/1132739184060489729
89.
by kobebrookskC3 5y ago
how about https://www.chromium.org/Home/chromium-security/memory-safet... https://langui.sh/2019/07/23/apple-memory-safety/ these companies apply things like sandboxing and fuz
90.
by kobebrookskC3 5y ago
for another operating system, we have ~70% of security bugs being memory safety issues ( https://www.zdnet.com/article/microsoft-70-percent-of-all-se... ). sounds like a decent majority to me.

More ›