Want to read Slashdot from your mobile device? Point it at m.slashdot.org and keep reading!


Forgot your password?
Check out the new SourceForge HTML5 internet speed test! No Flash necessary and runs on all devices. ×

Comment Re:Because Windows Sucks (Score 5, Insightful) 265

The only reason Linux is perceived as more secure than other operating systems is because most hackers don't care enough to spend time working to crack it, so there are less attempts.

Linux is a major server OS (arguably the largest), very big in embedded systems, and completely dominant on smartphones. Hackers are spending very significant time working to find exploits.

Comment Re:Or stay on LTS (Score 1) 78

I'm using LTS for all my work machines. The last round I rarely felt I missed out on anything compared to my updated machine at home. I think it's perfectly reasonable to stay with LTS if you want. You can still update to newer versions of, say LibreOffice and similar applications using snaps if you need it.

Comment Re:Newsreels (Score 1) 348

Fantasy. DRM and the DMCA make reverse engineering and backup impossible.

OP was talking about analog reels made decades before digital film and the DMCA. Yes, the DMCA effectively castrates fair use and other provisions of copyright law when dealing with digital media that has anti-circumvention mechanisms in place but that has nothing to do with the topic at hand.

The more pressing issue is much of this media is physically controlled by entities that have zero incentive to digitize or distribute it. The relevant laws here would be about trespassing or theft, as one would need to break into a vault and physically steal reels to do anything with the material.

Comment Re:Formal verification is worthless IRL. (Score 1) 531

I love that people can and do undertake this type of thing. It's good for the development and improvement of the state of the art, continued research is valuable purely as research and I don't really want it to stop.

It's also so far removed from pragmatic non-academic reality that it's insane.

SYSGO is a pretty pragmatic non-academic company that has existed in reality since 1991.

Three years, and found two bugs?

Keep in mind that PikeOS was already used in automotive and avionic systems, so it was already rigorously developed and tested. It is indeed quite a testament to the quality of the product.

Let alone the obvious risks around the complexity, completeness and accuracy of a model that took so long to develop.

This model was developed exactly because existing models and theories could not be applied to real-life systems such as the PikeOS microkernel. The papers I linked earlier explicitly discuss managing the complexity.

The EAL link is interesting though, hadn't come across that before.

I hope you are not working on safety-critical systems then.

I suspect most of the systems I work on would qualify at EAL4 but the cost of demonstrating it would kill their commercial value; we'd discontinue the products rather than waste the money.

In the industries where this currently matters, it is the same: you either get your certification (this, or another one depending on the field) or you discontinue the product since you are not allowed to sell it at all (or rather: your prospective customers are not allowed to use it).

EAL7? Comically that's more likely - but only for key algorithms we develop and use. A whole system? Could take down the company..

Another part of the project was about formalising the MILS (multiple independent levels of security) architecture, which enables you to compose components certified at different levels (EAL or otherwise) in a way that does not bring everything down to the level of the least certified component.

And indeed, you will almost never certify an entire system at EAL7.

Comment Re:Formal verification is worthless IRL. (Score 1) 531

constructed a formal model of the PikeOS separation kernel

How long did this take?

The EU project lasted 3 years. Before they could model the kernel, the formal modelling guys had to extend their modelling environment. There were two guys from SYSGO (developers of PikeOS) working (very) part-time on this, two senior researchers from universities, and then some graduate students (I don't think more than two).

Did it actually add any value?

They found 1.5 bugs in PikeOS with it: 1 real bug, and one theoretical bug that could not occur in practice due to the limitations of the API in which it was found (but it was fixed anyway, since you never know whether someone might want to extend it at some point).

Additionally, formal modelling is also a requirement for higher levels of certification, which the PikeOS developers want to reach.

Would it have been quicker to just rewrite PikeOS?

Which language and what development methodology would automatically have the same results as the existing working product and its associated formal model?

Comment Re:Formal verification is worthless IRL. (Score 4, Informative) 531

When you write a program that needs to print the primes up to a certain number, you can easily create a formal proof that your program program is correct.

But when your program is say "apache", that needs to interact with many different browsers on one side, and interpret PHP scripts that interact with databases, this formal proof becomes impossible. Similarly, you cannot write a formal spec for the interaction with the user in for example, a web browser.

While things like the halting problem obviously prevent fully formally proving the correctness of programs, you can go much farther than we generally go today. For example, I participated in an EU project where they constructed a formal model of the PikeOS separation kernel (kind of like an embedded real-time hypervisor). They also generalised this model, which includes support for things like interrupts and context switches.

Comment Re:Why bother? (Score 4, Informative) 49

It's the principle of the thing.

Apple is winning against these requests from the government, but barely. Wikipedia says that a judge ruled in their favour in Brooklyn, but in the most publicized case - the case of the San Bernadino terrorists, the FBI withdrew their request rather than have Apple's objection decided on by the judge.

Dragging these assholes into the sunlight and making their methods a matter of public record makes things better for everybody.

Slashdot Top Deals

Every young man should have a hobby: learning how to handle money is the best one. -- Jack Hurley