Oxford Uni has its own police force that (IIRC and I think I do) has the same powers as UK police within X miles of Carfax Tower at the centre of Oxford (where X is about 5). So the local police handing back to the University police doesn't get the students off the hook very much... It's practically impossible to secure a network which spreads as widely as the University network does. Each college, and there are over 30 of them, has access to it. Planting a sniffer really isn't rocket science. And the "Oxford Stunted" is renowned for the quality of its investigative journalism, but not in any good way...
To prove the correctness of an (Integer) square root routine you would specify something like:
procedure Sqrt(X : in Integer; Y : out Integer) --# derives Y from X; --# pre X >= 0; --# post (Y*Y <= X) and ((Y+1)*(Y+1) > X);
i.e. Y, your sqrt, is no more than X when squared, but increase it by 1 and it is more than X. You require X to be non-negative.
Assuming that your implementation implements an initial guess at Y and then repeatedly increments it, you would specify a loop invariant that shows that your guess at Y (say 'Z') is such that (Z+1)*(Z+1) For more information on what's practicable in a customer-specified system, read the peer-reviewed publications...
Ada functions can have side effects; SPARK functions can't (that is, if they do have side effects, these will be detected by the analysis tool and generate an error). Also, you can't have recursive subprograms (directly or indirectly recursive).:-)
Postconditions are useful for proving partial correctness, i.e. correct if the subprogram terminates. They are useful because, in general, it is easier to specify a constraint than implement it - see how much easier it is to program in declarative (functional) languages than in imperative. (And Ada allows fixed point arithmetic, which is easy to reason about, and floating point arithmetic, which is harder to reason about but not impossible).
I telephoned SCO in the UK (my local branch) yesterday. I wanted to know what I, as a personal Linux user, had to do to licence my OS or change it to avoid infringing. After a short delay I was forwarded to a lady who told me that they didn't have any information packs on infringement, but that as a personal user "I didn't have anything to worry about".
When pressed, she gave me the number of the SCO Utah office 1-801-765-4999 (as specified on the SCO web site for further information.
So everything is OK folks -- SCO can't possibly go after home Linux users without having this waved in their face. I'm quite happy to sign an affidavit about these events. I'd also suggest that any worried US/CA Linux users give SCO Utah a call and ask for information on how to avoid infringement. Better safe than sorry!
SCO: We're Not Just Evil, We're Not Even Good At Being Evil.
Re:LinuxBIOS in flight computers
on
In-Flight Reboot?
·
· Score: 2, Interesting
It's not quite that simple.:-) If you are running a safety-critical system such as the arming system or stores management system then safety and procurement regulations require you to use a high-integrity operating system / programming runtime. Given the four levels of integrity defined in RTCA DO-178B (the bible for USA avionics software), this sort of software runs at Levels A or B (high integrity); even cut-down and much-tested Linux is only really suitable for Levels C or D.
If you want software that does not crash during operation, you have to remove subroutine recursion and dynamic memory allocation so that you can guarantee an upper bound on the stack and pool usage at any time. If you're using multiple processes then you need some way of preventing deadlock and livelock. Whether you use C, C++ or Ada, you have to enforce these conventions in some way. See the SPARK Ada site for an example of how you do this. But fundamentally, to write software that is crash free you cannot take an off-the-shelf language and off-the-shelf OS and simply hope for the best.
There is no substitute for a competent programmer if you wish to write secure code. There is equally no substitute for a well-designed language, nor for effective tools to support programming in that language.
The safety-critical software community has been tackling these very issues for the past fifteen years or more; the security community is sometimes guilty of re-inventing the safe software wheel, and doing it badly.
Safety engineers have already come up with the MISRA C subset (here) and tools to enforce it, but the general conclusion appears to be that C (and C++) are inherently unsafe languages and there's only so much you can do to patch over the problems.
If programmers are serious about wanting to write correct code, they are going to have to check their egos at the door and use tools that tell them where they are going wrong as early as possible. My personal suggestion is the
SPARK Ada subset and associated toolset, but then I'm biased.:-)
Take a little longer over your code. Get it right first time. Write your tests before you write the code. Use static analysis tools that are proven to pick up real errors. But enjoy what you're doing, because the best programmer in the world is still going to produce crap code if he's bored...
FPGAs are great in prototyping when you want to produce a relatively small number of devices in a relatively short time. Problem is, a conventional microprocessor is always going to beat an FPGA at a comparable VLSI design level in terms of flexibility, and an ASIC will draw less power and perform a specific task more quickly. Limiting factor for an ASIC is cost (minimum production runs often in thousands) and design-production latency.
If you want to emulate an Athlon, use an Athlon.:-)
Stuff like high-volume encryption (e.g. Rijndael) is well suited to FPGAs because you've got a shedload of data coming in for a relatively simple series of calculations. Note that the AES contestants were evaluated partly on their ease of implementation in FPGA-like devices.
This SDRAM link might be a useful thing to increase bandwidth between a conventional microproc/bus/memory system and multiple FPGAs, bumping up performance by a factor of 2-3 maybe (on bandwidth-limited computations), but it won't change the world. IMHO, obviously.
Check out my review of the FPL 2000 and FPGA 2001 conferences for summaries of the current research in FPGAs.
An actual benchmark here. I had a Christmas puzzle that involved placing 4x4 tiles so that coloured patterns on the edges matched. Failing to do it manually, I wrote a Haskell program to solve it -- 2 hours to write, 20 seconds to run, gave all the solutions. I then developed a C program to do the same thing. About six hours to write, less than 2 seconds to run.
Haskell is cool. But, like any other language, it is only suitable for a certain class of problems. Use it outside that, and suffer.
This basic approach has been done for a while in the safety engineering field with fault trees; take all the existing comments by Bruce and replace "security" with "safety". The idea of applying the model to security is an interesting one, and indeed in many cases safety engineering can become effectively security engineering.
The typical safety approach using something like Fault Trees starts off with an aim of a safe system, identifies the principle hazards to that system (e.g. bomber releasing an armed bomb in a closed bomb bay), then works down decomposing those hazards using AND/OR junctions to reach a list of specific things which we have to prove about the system (e.g. no software write to location 0xf0001234 which is not immediately preceded by a check of the Bomb_Bay_Open sensor).
See http://www.cs.york.ac.uk/hise/ for and Nancy G. Leveson's book "Safeware" for more info on safety engineering. My post doesn't even scratch the surface of the subject.
Slashdot Mirror
Oxford Uni has its own police force that (IIRC and I think I do) has the same powers as UK police within X miles of Carfax Tower at the centre of Oxford (where X is about 5). So the local police handing back to the University police doesn't get the students off the hook very much...
It's practically impossible to secure a network which spreads as widely as the University network does. Each college, and there are over 30 of them, has access to it. Planting a sniffer really isn't rocket science.
And the "Oxford Stunted" is renowned for the quality of its investigative journalism, but not in any good way...
i.e. Y, your sqrt, is no more than X when squared, but increase it by 1 and it is more than X. You require X to be non-negative.
Assuming that your implementation implements an initial guess at Y and then repeatedly increments it, you would specify a loop invariant that shows that your guess at Y (say 'Z') is such that (Z+1)*(Z+1) For more information on what's practicable in a customer-specified system, read the peer-reviewed publications...
Disclaimer: SPARK hacker for 6 years
Ada functions can have side effects; SPARK functions can't (that is, if they do have side effects, these will be detected by the analysis tool and generate an error). Also, you can't have recursive subprograms (directly or indirectly recursive). :-)
Postconditions are useful for proving partial correctness, i.e. correct if the subprogram terminates. They are useful because, in general, it is easier to specify a constraint than implement it - see how much easier it is to program in declarative (functional) languages than in imperative. (And Ada allows fixed point arithmetic, which is easy to reason about, and floating point arithmetic, which is harder to reason about but not impossible).
Disclaimer: SPARK hacker for the past 6 years.
When pressed, she gave me the number of the SCO Utah office 1-801-765-4999 (as specified on the SCO web site for further information.
So everything is OK folks -- SCO can't possibly go after home Linux users without having this waved in their face. I'm quite happy to sign an affidavit about these events. I'd also suggest that any worried US/CA Linux users give SCO Utah a call and ask for information on how to avoid infringement. Better safe than sorry!
SCO: We're Not Just Evil, We're Not Even Good At Being Evil.
If you want software that does not crash during operation, you have to remove subroutine recursion and dynamic memory allocation so that you can guarantee an upper bound on the stack and pool usage at any time. If you're using multiple processes then you need some way of preventing deadlock and livelock. Whether you use C, C++ or Ada, you have to enforce these conventions in some way.
See the SPARK Ada site for an example of how you do this. But fundamentally, to write software that is crash free you cannot take an off-the-shelf language and off-the-shelf OS and simply hope for the best.
There is no substitute for a competent programmer if you wish to write secure code. There is equally no substitute for a well-designed language, nor for effective tools to support programming in that language.
The safety-critical software community has been tackling these very issues for the past fifteen years or more; the security community is sometimes guilty of re-inventing the safe software wheel, and doing it badly. Safety engineers have already come up with the MISRA C subset (here) and tools to enforce it, but the general conclusion appears to be that C (and C++) are inherently unsafe languages and there's only so much you can do to patch over the problems.
If programmers are serious about wanting to write correct code, they are going to have to check their egos at the door and use tools that tell them where they are going wrong as early as possible. My personal suggestion is the SPARK Ada subset and associated toolset, but then I'm biased. :-)
Take a little longer over your code. Get it right first time. Write your tests before you write the code. Use static analysis tools that are proven to pick up real errors. But enjoy what you're doing, because the best programmer in the world is still going to produce crap code if he's bored...
Adrian
FPGAs are great in prototyping when you want to produce a relatively small number of devices in a relatively short time. Problem is, a conventional microprocessor is always going to beat an FPGA at a comparable VLSI design level in terms of flexibility, and an ASIC will draw less power and perform a specific task more quickly. Limiting factor for an ASIC is cost (minimum production runs often in thousands) and design-production latency.
If you want to emulate an Athlon, use an Athlon. :-)
Stuff like high-volume encryption (e.g. Rijndael) is well suited to FPGAs because you've got a shedload of data coming in for a relatively simple series of calculations. Note that the AES contestants were evaluated partly on their ease of implementation in FPGA-like devices.
This SDRAM link might be a useful thing to increase bandwidth between a conventional microproc/bus/memory system and multiple FPGAs, bumping up performance by a factor of 2-3 maybe (on bandwidth-limited computations), but it won't change the world. IMHO, obviously.
Check out my review of the FPL 2000 and FPGA 2001 conferences for summaries of the current research in FPGAs.
Adrian
Haskell is cool. But, like any other language, it is only suitable for a certain class of problems. Use it outside that, and suffer.
Adrian
PS What happened to Orwell?
The typical safety approach using something like Fault Trees starts off with an aim of a safe system, identifies the principle hazards to that system (e.g. bomber releasing an armed bomb in a closed bomb bay), then works down decomposing those hazards using AND/OR junctions to reach a list of specific things which we have to prove about the system (e.g. no software write to location 0xf0001234 which is not immediately preceded by a check of the Bomb_Bay_Open sensor).
See http://www.cs.york.ac.uk/hise/ for and Nancy G. Leveson's book "Safeware" for more info on safety engineering. My post doesn't even scratch the surface of the subject.
Adrian
Speaking for myself, not for my employer