nanolith

30 ms·

301.
by nanolith 10y ago
Case in point: cryptography, authentication, and authorization are each very sensitive operations which are prone to both gadget attacks and sidechannel attacks. Sandboxing these operations by creating well-defined boundaries between appli
302.
by nanolith 10y ago
If done well, formal verification of kernel level services and how these use runtime protection built in hardware can absolutely reduce the attack surface of application level code. The key is to move critical services that attackers would
303.
by nanolith 10y ago
It is upon the shoulders on these giants where I stand. Dijkstra, Floyd, Hoare, Knuth, Curry, Church, and Turing, among others. The science exists. The trick now is bringing it all together in a way that is useful enough to others that th
304.
by nanolith 10y ago
I agree with your synopsis on Pastebin. It's pretty close to what I have been trying to practice. As an interesting aside, I worked with a few researchers about a decade ago on tracking SMM vulnerabilities in various Intel chipsets.
305.
by nanolith 10y ago
"Also true for many embedded apps given the remaining runtime hit can range from single-digits to 40% depending on scheme used." I think that depends on the definition of embedded. When one is lucky enough to work with a chipset
306.
by nanolith 10y ago
Compiler transformation can solve most of these concerns, but it is not perfect due to undecidability. Compiler transformations will always be conservative, falling back on runtime enforcement. The main edge cases I've run into -- hen
307.
by nanolith 10y ago
Yes. But, you typically have to use a theorem prover to build up static checking for functions, and then enforce proof obligations on callers to said functions. If done in a system like Coq or Isabelle, the proof obligations become a para
308.
by nanolith 10y ago
MAC-then-encrypt is a pet peeve of mine. It is so much safer to apply the message authenticator AFTER data has been encrypted, after which point it protects both the cipher text and the underlying plain text. Yes, I'm aware that ther
309.
by nanolith 11y ago
It could be larger, but it would be a known constraint with known runtime characteristics. There is value in this, especially with regards to understanding the worst-case performance.
310.
by nanolith 11y ago
Something interesting that isn't covered in this blog entry but is relevant to many of us is the importance of deterministic parsers for DOS / DDOS prevention. APIs that make use of parsers, be they regular expression parsers, or
311.
by nanolith 11y ago
I have read much of it. It's a project I started in my late teens, and have revisited many times over the subsequent twenty years. I have done many of the (simpler) exercises, and I have even sent in a letter detailing a small error
312.
by nanolith 11y ago
I guess I should have clarified that "reliable and predictable" performance is critical. In practice though, these systems have fast enough context switching. I agree with you that "fast enough" is the only metric that
313.
by nanolith 11y ago
I would love to see some blog posts regarding your experience during this internship. I am working on some formal verification myself for some commercial projects, and I enjoy reading about stuff like this.
314.
by nanolith 11y ago
I saw a sibling reply posted shortly before mine outlining your work. Nice job. :-)
315.
by nanolith 11y ago
Well, most microkernel vendors have niche markets that aren't directly competing against Linux. Minix 3 is a bit of an outlier. Although it is a desktop and "server" OS like Linux, it's really meant to be more of a tea
316.
by nanolith 11y ago
Not much, really. The main thing needed is to port the language runtime to seL4. This should be a relatively small effort, and a great project to both learn some of the underbelly of Rust's ABI and seL4.
317.
by nanolith 11y ago
Certainly, having a well-defined interface makes both empirical testing and portability easier. Microkernels get this by default. To be fair though, modern monolithic kernels have pretty decent abstraction mechanisms that do make it easy
318.
by nanolith 11y ago
One thing that is much easier to do in a microkernel than in a monolithic kernel is build a machine-checked proof of correctness. This is not to say that this cannot be done in a monolithic kernel, but the proof would have to extend to eac
319.
by nanolith 11y ago
It is my goal to open source the tool at some point in the near future. I have a few IP related things to work out with my employer first, as a courtesy.
320.
by nanolith 11y ago
I use a similar workflow using Pandoc at work. I painstakingly re-created our corporate Word documentation templates using LaTeX and then set up Pandoc to generate documents from Markdown using these templates. In addition to this, I used
321.
by nanolith 11y ago
You're right. It's not as pure as mathematics. But, it is much purer and cleaner than a lot of languages in use today. It lends itself well to translating into formal proofs, and it is a great testing bed for ideas. Haskell ha
322.
by nanolith 11y ago
Yeah. There can be no doubt that there are plenty of companies that have failed to grasp the point of the technical interview. I've had to coach employees in the past because they often gravitate towards silly questions like "na
323.
by nanolith 11y ago
Being able to reason about a problem and then work towards a solution in code is a more general skill than just programming or CS. I'm assuming that here, "FizzBuzz" is more of an allegorical example than a literal test ques
324.
by nanolith 11y ago
I've interviewed for top technical companies in Silicon Valley and have gotten job offers. I've never encountered a scenario as dire as the one you paint. Rarely do these problems go beyond something that can be reasoned out on
325.
by nanolith 11y ago
The point of these tests is not to see who remembers their CS. The point of these tests is to have an opportunity to see how candidates go through the process of solving problems by approaching a problem that is well-understood by the inte
326.
by nanolith 12y ago
I would love feedback regarding usability and feature requests. I have started using this framework for internal testing, but I'd love to see it used by others.
327.
Show HN: Portable Mocking Framework for C++11(github.com)
1 points by nanolith 12y ago|1 comments
328.
by nanolith 12y ago
I fondly remember reading the print editions of both Dr. Dobb's Journal and the C/C++ User's Journal (later folded into DDJ). Part of me misses this sort of curated content. Getting an article accepted in such magazines got
329.
by nanolith 12y ago
Actually, I didn't ignore that in my original comment. I mentioned that the GNU Emacs work should make use of a file format which is independent of the plugin work. There is no reason why GNU would refuse to mainline such an enhancem
330.
by nanolith 12y ago
CMake is another useful tool. It has fewer dependencies than SCons and is significantly faster. The only downside is that CMake scripting has a steeper learning curve because it is so different than other build systems. On the other hand

More ›