On Tue, Sep 9, 2014 at 7:29 PM, Matti Karnaattu <mkarnaa...@gmail.com> wrote: >>Also if you were to provide more specifics about your goals, others may >>have more input. > > At the moment I'm looking hobby project to maintain/improve my skills > developing open source software and my goal is to develop/improve some > open source component(s) to be suitable on safety critical use.
"hobby" and "safety critical" don't often go together. if you just want to improve your skills i say go for it but aiming for safety critical is a high bar to achieve. But if you're really looking to do safety critical, which industry are you going to target? is it aviation (hope you're well versed in DO-178C), automotive (you've looked over ISO 26262 and MISRA C, right?) nuclear, medical? something else? Not exactly light reading or easy to achieve... > > What I need is some place to start, and starting point is to find > developer community whose interest is quality code, sharing some same > values and suitable platform. Well, if a POSIX-like platform that pays attention to detail is one of your goals, then OpenBSD is one of the cleanest places to start in my biased opinion. > >>On the other for hard/soft hard real-time I might look elsewhere > > I'm looking possibility to isolate process on own CPU core because when > looking from safety perspective, it is bad thing if some other process > can jam CPU. Memory and hard drive isolation are easy tasks but if OS > have possibility to isolate CPU too, that opens new possibilities. > > If this can be done, it is not long way to improve real time > capabilities. I'm not sure I agree that memory isolation is an easy task. OpenBSD includes so many mitigation strategies against memory corruption for a reason. See: http://www.openbsd.org/security.html > > Not sure yet am I looking from right place. I just LOVE to browse > OpenBSD source tree. It is clean in many ways, simple and I have found > it to be realiable. However, it is unclear what are interests of OpenBSD > developers and where project is heading. These are listed on the interwebs: http://www.openbsd.org/goals.html > > I consider that going deep kernel internals is out of scope for my > interests so some developer hacking kernel every week should have > interests to enable OpenBSD suitable for safety programming. Otherwise I > have to look elsewhere. The only person who will mold things around your interests is *you*. > >>Can you give more details about what tools/techniques you have in mind? > > Formal specifications defined with modified condition/decision coverage, > model checking, automated theorem proving etc. To get that point, I have > to use heavy static analysis to clean code to the point that it can be > tested > thoroughly. Ah, so MC/DC makes me think you're interested in DO-178B/C. Ok, but this is a somewhat questionable/controversial technique, no? Interactive theorem proving is used heavily in sel4 as far as I know, so that might be a more interesting place for you to look rather than OpenBSD. It's pretty interesting work and it's open source. Static analysis, on the other hand, has been used extensively on the OpenBSD code base over the years with some good success. More work could certainly be done on this front though. Patches addressing bugs found through static analysis are always welcome. > > OpenBSD is aiming security and using proactive methods + code auditing > to achive that, but proving that some pieces of code are correct raises bar. > Zero defects means zero security holes. Sure formal methods could help. If you do something using formal methods then by all means, feel to submit patches. If you stay on this list long enough you'll learn that people consider talk to be cheap... And remember just because you've formally proved some piece of code is free of buffer overflows doesn't mean you've proved there are no security holes.
