Slashdot Mirror
Apple Security Blunder Exposes Lion Login Passwords In Clear Text
An anonymous reader writes "An Apple programmer, apparently by accident, left a debug flag open in the most recent version of its Mac OS X operating system. In specific configurations, applying the OS X Lion update 10.7.3 turns on a system-wide debug log file that contains the login passwords of every user who has logged in since the update was applied. The passwords are stored in clear text."
now i can find out what my password is.
ive been resisting a reboot for ages!
apple even ships their own malware.
It's a good job that my password is also the combination to my luggage.
In before "lol Mac users deserve this".
That makes for quite the dangerous security breach.
When I build a system for Linux distribution, I use scripts to configure the options on the build server. I don't use manually specified configurations from developer workstations.
Doesn't Apple grasp this concept of source code versioning and build management? Or was the debug flag in question hard-coded in the source rather than specified as a build option? If so, Apple needs to revisit it's coding structure and figure out how to set BUILD TIME options instead of hard coding them.
I do not fail; I succeed at finding out what does not work.
...There is app for that.
sed -e 's/Chuck Norris/Rajnikant/g' joke > fact
...I've got to say that if a fellow pen-tester managed to find a really deep, complex and convoluted vulnerability in by code then that's fair game and kudos to him.
This though...bitten by a debugging flag, the dev must be hitting the sauce right about now.
Now, putting my coder hat back on, why was a debugging flag left enabled while building for production?
That's just lazy/bad setup, everyone knows that you keep your environments separate.
I wonder what the source code or version control comments said..
Actually, Lion's FileVault is not a problem. Only if you were using the old FileVault from previous OSes (which only encrypted the home folder), upgraded to Lion, but did not switch to the new full disk encryption FileVault for some strange reason.
For a Debugging Log. As the article said.
Your login password also unlocks the encryption password for FileVault. The login passwords were apparently logged in a file outside of the encrypted image. (Only for the old pre-lion version of FileVault running under Lion)
Anyone who used FileVault encryption on their Mac prior to Lion, upgraded to Lion, but kept the folders encrypted using the legacy version of FileVault is vulnerable. FileVault 2 (whole disk encryption) is unaffected.
I can see how those circumstances could occur in the real world; however the first version of FileVault was a pain, and I don't know of many people that kept using it for very long.
I stopped using FileVault v1 after a few days. What sensitive stuff I have is now in encrypted sparsebundles, with the rest of my stuff unencrypted. Time Machine backups are stored on a LUKS-encrypted disk.
FWIW I've stuck with Snow Leopard - not a real fan of Lion. That was another thing I stopped using after a few days, although I did like the whole-disk encryption option.
#DeleteChrome
From TFA, the specific configurations that allow this to happen: "Anyone who used FileVault encryption on their Mac prior to Lion, upgraded to Lion, but kept the folders encrypted using the legacy version of FileVault is vulnerable. FileVault 2 (whole disk encryption) is unaffected."
FTA:
So only certain configurations, and relatively few at that.
things such as debug logs during testing.
Does Apple have no such thing? This leads me to think that Apple either has no development lifecycle or, in case they have one, only half-heartedly obey it.
Viable Slashdot alternatives: https://pipedot.org/ and http://soylentnews.org/
You missed the gp's point. At what point do you need to see the passwords in a debugging log?
You are wrong my friend. It's your disbelief that makes you see us sitting down but in reality we do no such thing.
-- Cheers!
...you're passwording it wrong.
Some "strange" reason?
How about you've got multiple users on the machine? With Filevault2, any user can unlock the whole disk. As much as I like macs, it's a complete joke. With Filevault1, you had homedir encryption on a per-user basis. My files were secure from other users of the machine.
Why in our time somebody, anybody would need passwords to be stored for log purposes at all? You need to check if the user is typing it the right passwords? Compare the encrypted versions and store a state saying: correct / wrong password was used, what else do you need?
Ask the rogue Google engineer who did this.
Looking at the actual message, it looks like the dev in question just took an "attributes" NSDictionary argument and stuck it into his NSLog() call whole hog, as in:
NSLog(@"about to call _premountHomDir with %@", attributes);
"%@" in an OSX printf-style format string will call -(NSString *)description on whatever object in on the vararg position for that %-code, and put that string in the output. The "description" selector on a dictionary spits out the keys and values of the dictionary in a human-readable format. The "attributes" object in this case contains a lot of information that would be interesting for a human debugger, the password being an exception.
Don't blame me, I voted for Baltar.
If you want to get hold of a colleague's password?
No. *Now* it can be avoided. Tests are for known (and therefore fixed) security problems, so they are only good for checking if the same bug is back. What happens in software development disturbingly often.
Contrary to the popular belief, there indeed is no God.
What? Something seriously missing from the summary!
Copying features from Microsoft products again.
I don't always use unix-like operating systems; but when I do, I prefer FreeBSD.
No, it's off by default, and if you don't use FileVault (the legacy version) you are effectively not effected - your disk is not encrypted to begin with, and thus starting the machine in target disk mode gives access to your home folder to an attacker (or they can reset your login password with the OS X installer), bit *not* your keychain password which is the same by default, but not if the login password is changed via the root user or another admin).
It's still a bit of a huge security blunder though.
I might suggest that your endorsement might have given several people a reasonably compelling reason not to use it.
If you sincerely are advocating that product, you may want to consider altering your sales pitch so that you don't sound so much like a snake-oil sales vendor. Otherwise, you just sound like a raving lunatic.
Of course... if that was your intent. Carry on. Expect to be downmodded, however.
File under 'M' for 'Manic ranting'
Indeed. Secret info in log-files is also a decades old problem. Any competent software developer knows about this and any bright person will figure it out by themselves. Guess the developer(s) in question are neither bright nor experienced. ElCheapo software development at its best.
Most ACs are not even worth the keystrokes to insult them. Be generically insulted by this and ignored otherwise.
If the test is checking log files, it's 1) not a unit test and 2) broken.
Dilbert RSS feed
All of his friends went over to work on iOS and he's been left to pick up the slack. ;)
Now I will have to change my password from "password" to "12345678."
--
A woman once said to Adlai Stevenson, "Every thinking person in America will vote for you," to which Stevenson replied, "That won't be enough, ma'am, I need a majority."
Because this is problematic if one's login password on a mac happens to be their login password for everything else inside of one company.
Odds are that firewalls will protect outsiders from being able to snoop, but what's to stop somebody on the inside from doing a little covert snooping to discover the administrator's password, and using that to his own advantage in some way?
I would rather hope that Apple addresses this issue before the work day commences tomorrow, because now that this vulnerability is publicly known, it's a shoo-in that it is going to be exploited.
File under 'M' for 'Manic ranting'
What qualifies that statement? Any FileVault user that upgraded to Lion would be affected, which I would think would be more than a few. FileVault is not upgraded to FileVault 2 automatically. The user would need to manually disable FileVault and then re-enable it to get the whole disk encryption feature.
All classes of tests are extremely limited in their usefulness. Some are just peddled better.
Contrary to the popular belief, there indeed is no God.
Somehow I have a feeling that if this same kind of "bug" had been found in another operating system, such as one coming from Redmond, the discussion and media coverage would have been quite different, and there would have been much more Slashdot comments on this story.
We are talking about passwords stored in clear text, no fix yet, and based on the article, no assurance that the fix would remove copies of the unencrypted passwords. For a company that was wondering how to spend 100 billions. What a joke.
lucm, indeed.
Underhanded C contests prove that it's possible to slip a bug into a critical piece of software in such a way that it looks like programmer error. This allows for plausible deniability from the company (Apple).
http://en.wikipedia.org/wiki/Underhanded_C_Contest
Don't bait the meth-fueled troll, and especially not from a named account if you know what's good for you. Have you been paying attention to just how widely he's doing this, how many accounts here (at least six as of right now), how many other sites he's poisoned? There's also a bizarre theistic reference in most of the account names used. Don't debate this freak, use the Flag button next to EVERY one of his posts in every guise, and let the admins with better weaponry deal with him.
It's a feature designed to enhance privacy by encouraging the user to change their password more often.
Specifically, at each login. And logout. And several times in between. Quick! Keep changing it!
"We live in a global world" - Harvey Pitt, former Securities and Exchange Commission Chairman
First, if you timestamp it, you don't need to salt it. The password would effectively have a lifetime of minutes at best, so adding a salt doesn't improve anything.
Second, your idea ruins the whole point of using a trapdoor function (what the internet means by "hash"). The point of the trapdoor function is that the server doesn't have to have your password stored on it, because you can just verify the password presented by comparing a hashed form of the presented password to the hash you have stored.
But with a time+password hashing scheme, the server must know the user's password because each time the user logs in, the must construct a new hash from the password and the current time.
So, if your server is going to know the password, just use a shared secret system like SRP. Then you get two-way mutual authentication too.
http://lkml.org/lkml/2005/8/20/95
What if the next bug leaks pasword backwards? In BASE64? Only on Mondays?
You can't test quality into the system. Tests can merely show that something is terribly, terribly wrong, and likely you have deeper problems.
Contrary to the popular belief, there indeed is no God.
After a year of having to endure "Your old Mac Core2 Solo 32bit can't RUN 64bit-only Lion! Loser!" comments, now, NOW I can say, there is a darn good benefit to staying behind the times! This security issue does not affect me!
This totally refills my Apple User Smugness supply.
Sig for hire.
That's what encrypted sparsebundles are for, surely (that you can mount at login).
FileVault 2 assumes that multiple users of the same system are mutually trusting of each other. It was not really meant to service multiple users - that's how version 1 worked and it had nothing but issues.
Although I'm not particularly a fan of Test Driven Development, you could have created some sort of 'debug flag disabled in release build' test the moment you decided to log passwords in clear text. You can even create a general rule like "Everytime you decided to weaken security for debugging purposes you should create a test that confirms this code will not be included in the release build". But yeah, without knowing much about their build process, its just pure speculation at this point and anyone can tell you how this problem can be avoided in hindsight.
But regarding tests, there are various useful tests that can test previously unknown program states. Especially stuff like fault injection testing is incredibly useful. In fact many security researchers find tons of tricky bugs using these techniques. for e.g. send randomized input strings to test for reliability of API interfaces which accept arbitrary strings, or you can use a test suite that 'randomly' makes the system go Out Of Memory to see how different services deal with it reliably, etc.
Bad Summary! Blah blah Modpoints blah blah TFA blah blah Apple blah blah...
Off topic, almost certainly. Idiotic, without a doubt.... but not actually inappropriate or offensive unless a person is offended by people who sound nuts.
File under 'M' for 'Manic ranting'
Much as it probably is hard for people to acknowledge, Apple doesn't hire the best and brightest. Historically, like Microsoft, they have bought in most of their 'innovation.'
They spent many many millions of dollars trying to produce the 'next generation Mac OS (tagilent, pink, whatever including the one they called sagan until Carl Sagan sued them then they changed it to BHA (buttheaded astronomer..))
Then they gave up because their staff apparently was only producing botique crap and was much more interested in justifying one-button mice than writing good code.
So they bought NeXT and wrote a pretty layer on top of NeXTStep to use as their 'new' OS.
The next bug is the next bug. We are not talking about a bug here, at least not a direct bug. In this case somebody did something on purpose, which was to help during development but is definitely not ok in production.
It was one of millions things that happen in development. There is no way to count them all -- if developers had to record every instance of enabling or disabling various kinds of output, they would never have time for actual development.
This particular problem would not happen if there was a predefined way of producing debugging output, that is guaranteed to be never enabled in production builds. That would work even if no one ever tested anything. Because it's a matter of development infrastructure, not testing.
Contrary to the popular belief, there indeed is no God.
Could it be? Sure.
Could those tests also easily (and fairly trivially) be worked around by a developer just "trying to figure out what's happening" and accidentally checking in some bad code to a release branch? Sure.
It's very likely that Apple does builds where "CCFLAGS += -g -D__DEBUG__" doesn't get appended on the compile line. It's very likely that the developer who did this was trying to figure something out, got sloppy/rushed, and checked in something that hard-coded this behavior into the code, and that code - intended for test only - never got removed from the production build.
There's a million ways you could look for this sort of thing, and a million and one ways a developer could - accidentally, or maliciously - circumvent it by hard-coding (or removing) things intended to prevent this type of code from being compiled into production releases.
That doesn't excuse the sloppiness; But there's no way to prevent this sort of a thing 100% of the time - automated tests are useful, and could help minimize the risk, but you simply can't automate away dumb mistakes. The "best" way to have prevented this would probably be a change review by another developer familiar with the code who would say "whoa whoa, you checked in debug code, man" - presuming that second developer takes the time to actually review the change report.
Although I'm not particularly a fan of Test Driven Development, you could have created some sort of 'debug flag disabled in release build' test the moment you decided to log passwords in clear text. You can even create a general rule like "Everytime you decided to weaken security for debugging purposes you should create a test that confirms this code will not be included in the release build".
No.
There should be no tests. There should be a rule that disables all debugging output in production builds. And, of course, all debugging output should use the mechanism that disables output with aforementioned rule.
Once that is implemented, testing is absolutely irrelevant, unless you are trying to test gcc.
Testing is for finding out if you have screwed up. Quality comes not from testing but from not screwing up.
Contrary to the popular belief, there indeed is no God.
us mods can only hide it from people who don't read @ -1 ! :( But i have been reporting these as i see it to admins hoping for a nice IP ban.
Instead of just logging to some file, you call a function like "debuglog" or something like that. Calling any other kinds of logging functions for debugging is absolutely strictly verboten. This function should be very easy to call so noone would have a reason to use any other kind of output functions. If they need a different method for recording debugging information, a new debugxxx function must be written first with the appropriate debug flags. Anyone using cout or any other output, even in a temporary 2 minute test, is terminated on the spot.
The production build simply replaces these debugxxx functions by nop. Problem solved.
And if there is no debug flag? Just some print statements, or #ifdef's being removed, or something like that?
There's no way to guarantee that this problem will ever be caught via an automated test. You can (and should) certainly test for specific scenarios that you can think of, but there's no way automated testing can know the intent or possible ripple effects of changes the developer has checked in; "verify no debug information is included in the production binary" can be automated. "Make sure the developer didn't remove an #ifdef block that turns on / turns off clear-text password logging for this particular binary," is a different question, and really all you can say for sure via an automated test is, "the developer changed some lines of code, here's the diff."
It's possible that the developer's mistake *could* have been prevented, but automated testing is not a magic cure-all that can divine the intent of the developer, and in a situation like this, it's not a "security bug," - e.g., expoitable hole that allows an attacker to escalate privileges - it's a "security bad practice." There's not a lot an automated test tool can do to catch that. It can take informed guesses that something "might" be a risk, but at some point, you need to involve someone who knows the code, and have them inspect the changes to verify that the changes match the intent of the developer without implementing bad practices.
They say that all FileVault (1 and 2) users on 10.7.3 are affected, so I looked at the appropriate file (apparently no one on the Internet is speaking its path and file name) and found the lines marked DEBUGLOG, but my cleartext password wasn't there. Everything else is. I'm not saying the story is untrue; I'm looking right at a bunch of lines that say DEBUGLOG. I guess I somehow got lucky.
My files were secure from other users of the machine
The way I see it, the technical difficulties -- both manifest and potential -- of protecting users from each other on the same OSX system made FileVault 1 untenable. Every app (written by Apple or not) that put data into unprotected memory, swap, or disk was in principle leaking confidential information from the vault. You may have felt like your files were safe, and if you never turned on remote login or allowed fast user switching you were probably right, but the general multiuser case is full of attack vectors.
So while in principle the per-user protection was nice, in practice it inevitably full of holes. Rather than provide the illusion of inter-user security, Apple switched to full disk encryption in FileVault 2 -- something closer to what most of its users really needed anyway.
Whoa. Dude. Like, I think you meant to post that on /r/trees man.
No.
There should be no tests. There should be a rule that disables all debugging output in production builds. And, of course, all debugging output should use the mechanism that disables output with aforementioned rule.
What are you disagreeing with?
Testing is for finding out if you have screwed up. Quality comes not from testing but from not screwing up.
That is such a meaningless statement. Thats like saying programming is the process of introducing bugs in the codebase. Only after you write tests can you claim any such quality of code base. If quality does not come from testing then it does not exist other than in a programmers subjective opinions.
What are you disagreeing with?
I disagree with a recommendation to add more tests to improve quality.
Thats like saying programming is the process of introducing bugs in the codebase.
No, but "introducing bugs in the codebase, running tests and watching if they cancel each other out" is a very much appropriate description of software development process as practiced by incompetent people. I call it perma-debugging cycle.
Only after you write tests can you claim any such quality of code base.
Tests do not prove anything other than two programs, test and program being tested, producing compatible results. They can just as well be both wrong, and usually test is formally wrong due to the limited scope and implicit assumptions made by a programmer who wrote it.
However a more important question is, do you want to be able to claim something, or actually make it closer to reality? If the former, go ahead, and do all kinds of measurements, tests, up to daily drug tests for programmers. This is a kind of solution we have with airports and TSA now. If you want to have less bugs, make it difficult to write a bug. Build infrastructure. Have infrastructure enforce global rules (such as when debugging logging is available) so programmer who uses it doesn't have to do it every time he implements anything. Re-use code that can be reasonably expected to be correct. Have code reviews.
Once that is done, there may be some talk about any kind of tests outside QA and developer's own initiatives. Maybe.
If quality does not come from testing then it does not exist other than in a programmers subjective opinions.
Of course, it is subjective. You want an objective evaluation of quality? Here it is: all software is wrong. For every piece of software at any point in time there is (known or unknown) valid condition that causes this software to misbehave. This will change when the last bugfix will be committed to some project, and so far no one, ever, made a claim that such an event happened.
But tests???
Tests are the most subjective thing that one can imagine to evaluate software quality. They are written by people who believe that software must pass some rules to be correct. You know what else is an expression of rules that produce software output? Software itself! Write the same program twice, run on all possible inputs (including all timing conditions as they are input, too), verify that result is always equivalent from some objectively defined point of view (again, timing, protocols, interactions with other software and hardware). That would be the only test that guarantees anything at all (+/- bugs in equivalence verification, +/- bugs in test infrastructure, +/- common bugs in both implementations). Anyone willing to implement that as his testing procedure? No? Takes nearly infinite time? Then everyone is welcome to shut the fuck up about tests being "objective" or "guaranteeing" anything.
Contrary to the popular belief, there indeed is no God.
So basically you want people to improve the quality of their code base, without actually giving them any concrete and practical way to measure the quality? Also why, are you ranting? No-one in this thread has claimed that tests are some kind of silver bullet. They are an important indicator - as objective as humanly possible - within reasonable constraints of day-to-day software development (we are not talking about NASA level quality and formal proofs and all that crap) - that can be useful in enforcing that software is designed & implemented to be robust, and relatively bug-free.
Also you are wrong that tests cannot guarantee anything. When a human guarantees something to another human it is assumed to not be some kind of absolute statement. This *is* the common use (legal and general) of the term. Because otherwise you need some kind of perfect god like being which can evaluate products/services.
Sure he was not paid by M$?
So basically you want people to improve the quality of their code base, without actually giving them any concrete and practical way to measure the quality?
Yes! I want people to avoid writing bugs regardless of those bugs being detectable by tests. I want people who can think of any kind of rule that applies to software, to implement and enforce that rule in their software so it will be logically impossible to violate it, instead of devising a tripwire for any piece of software that visibly violates it.
Also why, are you ranting?
Because this line of thinking reveals one of the most poisonous traditions in modern software development -- writing something that "looks right", and only starting to think when something visibly fails in a spectacular way.
No-one in this thread has claimed that tests are some kind of silver bullet. They are an important indicator - as objective as humanly possible - within reasonable constraints of day-to-day software development
No, they are not. They are arbitrary checks for randomly selected egregious mistakes. Passing tests lulls developers into thinking that their software works correctly when it really does not.
(we are not talking about NASA level quality and formal proofs and all that crap)
Why not? For tests to be meaningful, the difficulty of writing them well exceeds the difficulty of writing formally-proven software. Step down from there, and sufficiently careful logical thinking (a step down from formal proof) will always beat an informal test (a step down from complete test) made with the same level of effort.
that can be useful in enforcing that software is designed & implemented to be robust, and relatively bug-free.
Practice shows that they do not improve quality, they teach people to write software that passes tests, and not think about the whole range of possible situations it has to deal with.
Good programmer writes software that not only behaves properly in all known corner cases, it works properly in those corner cases that he can't imagine. After some level (that is supposed to be long passed at the time of graduation from university), all trivial ways of improving quality already reached their limit and became irrelevant. Tests are among those methods. All further improvement can be only achieved by becoming an aforementioned good programmer, and tests don't in any way help with this. Just the opposite, writing code as if it will never be tested and there is no way to test it, is the only way to keep yourself from avoiding mistakes (even if the code is tested after that).
Also you are wrong that tests cannot guarantee anything. When a human guarantees something to another human it is assumed to not be some kind of absolute statement. This *is* the common use (legal and general) of the term. Because otherwise you need some kind of perfect god like being which can evaluate products/services.
So the purpose of tests is to create an impression of "proof" to people who don't know any better?
There is nothing wrong with testing products in QA, alpha testersm beta testers, etc. -- they just might find something by pure luck or pure stupidity of the programmers. There is nothing wrong with programmers writing mini-tests to check if they are completely off-base in their thinking. However those things have nothing to do with improvement of development process. They are helpful because they often catch brain farts, but they guarantee nothing. The better are programmers, the least helpful are tests, and long before programmers become perfect, tests become worthless. If a company can benefit from including mandatory tests into development process, it means that it's full of incompetent programmers, who should not be there in the first place. Same applies to marathon runners and crutches, and many, many other things that "assist" in a way that only works when something deeper is terribly, terribly wrong.
Contrary to the popular belief, there indeed is no God.
keep yourself from avoiding mistakes
Should be keep yourself from making mistakes, obviously.
Contrary to the popular belief, there indeed is no God.
They are arbitrary checks for randomly selected egregious mistakes. Passing tests lulls developers into thinking that their software works correctly when it really does not.
That is the way /YOU/ see tests. Most people use them to verify that very rule that you're talking about. Testing is not some random code that people throw together. It can be just as carefully written and as planned, if not more, than the actual software being tested.
Why not? For tests to be meaningful, the difficulty of writing them well exceeds the difficulty of writing formally-proven software. Step down from there, and sufficiently careful logical thinking (a step down from formal proof) will always beat an informal test (a step down from complete test) made with the same level of effort.
The development of tests can be done with multiple smart people. They can divide up the program however they want and implement tests for it. This is impossible with formal proof. Without a several iterations you will be unable to even divide up the code the be formally analyzed in parallel. Tests will always be a faster and commercially more superior solution.
Practice shows that they do not improve quality, they teach people to write software that passes tests, and not think about the whole range of possible situations it has to deal with.
Then that means those people sucks at writing tests.
So the purpose of tests is to create an impression of "proof" to people who don't know any better?
Depends on what you're doing. For a large softwares like Windows there are thousands of outstanding bugs and 90% of the users would not even recognize those bugs. Software will still be shipped and the bugs can be addressed in future updates. If you want a zero bug criteria then no software will ever ship on time. And all the companies will go bankrupt because there is no supply of software developers who are able to write that kind of software.
The better are programmers, the least helpful are tests, and long before programmers become perfect, tests become worthless.
This will never happen. Currently majority of software developers are employed by commercial companies. Their aim is to improve profit, not to make their employees better developer. Sometimes those two things can align because higher quality code means more profit, but that happens only a minority of the time. The other large section of software developers will be in academia. They have no clue about software development. They have never shipped anything robust because they have such low number of users that every code path is never tested in their code.
Late last Wednesday 9 May 2012, Apple released the OS X 10.7.4 update for both the client and server editions of the OS, that corrects this error and closes this security vulnerability, amongst other issues. The update is available thru the standard automated Software Update channel as a delta update for 10.7.3 users or as a combo update for all 10.7.x users, or as downloadable updaters found in http://support.apple.com/downloads/#macosandsoftware The delta update is around 400MB (700 for the standalone downloadable) and the combo update is around 1.3GB (1.55 for the standalone downloadable). From the official blurb:
The 10.7.4 update is recommended for all OS X Lion users and includes general operating system fixes that improve the stability, compatibility, and security of your Mac including fixes that:
Resolve an issue where the “Reopen windows when logging back in” setting is always enabled
Improve compatibility with certain British third-party USB keyboards
Address an issue that may prevent files from being saved to a server
Improve the reliability of copying files to an SMB server
For detailed information on this update, please visit this website: http://support.apple.com/kb/HT5167.
For information on the security content of this update, please visit: http://support.apple.com/kb/HT1222.
That is the way /YOU/ see tests.
This is also what happens when people use tests.
Most people use them to verify that very rule that you're talking about.
If rule can be expressed, it's possible to create code that always follows it. It may be possible to create code that verifies it (and therefore can be used for testing), but it's always more difficult and often plain impossible (ex: halting problem).
Testing is not some random code that people throw together. It can be just as carefully written and as planned, if not more, than the actual software being tested.
And then the result is still inferior to software being written right to begin with. However more likely tests are buggy, too, even if for some insane reason they are less buggy than software being tested. Tests only help to improve quality if they are written by a programmer far superior to the programmers who write software. This is why it works with teaching students. In all other situations they are merely an unreliable way to reduce the number of massive mistakes. Useful in the same way a guardrail is useful on a straight road -- its presence reassures the drivers that there is something at the edge of the road, and once in a blue moon someone will slam in it and won't die instantly in a ditch, but overall effect on the number and severity of incidents is negligible.
The development of tests can be done with multiple smart people.
And it would be more productive to just let those people write software.
They can divide up the program however they want and implement tests for it. This is impossible with formal proof.
Of course, it's possible! Software should be modular, with interface specifications defined for each module. Then all formal proofs or informal checks have to be done separately for each module, and for interaction model itself. Like with my example with the solution to a problem with debugging logs, once it is defined that a single interface must be used for all debugging logging, it's trivial just by looking at the code to determine that:
1. Debugging logging is never activated by default in production version.
2. All debugging information is logged through debugging logging interface.
So one implementation and one code review gives you very high certainty that all misbehavior related to debugging logs (information disclosure, performance drop, runaway use of space, use of log files as a part of privilege escalation or denial of service, etc.) will not happen on a production system in default configuration. Without this, you can test code until you are blue in the face, and billions of possible instances of debugging output will slip through your tests because they would be still indistinguishable from all other I/O.
When software is designed as a giant blob of spaghetti code, the problem is not with insufficient testing.
Without a several iterations you will be unable to even divide up the code the be formally analyzed in parallel.
If it is not already divided, it's designed poorly to begin with.
Tests will always be a faster and commercially more superior solution.
A solution to create false impression of correctness -- yes.
Then that means those people sucks at writing tests.
Just like in a well-known Kernighan's quote about debugging being twice as hard as writing code, so is writing tests (though I don't think, it's merely "twice", it varies with expected coverage). So everyone sucks at writing tests, and this is why a superior programmer can "rescue" an inferior one by providing tests. However this is like trying to use monkeys for building roads -- can work with enough effort applied by humans directing them, but it's easier to just let humans build those roads in the first place.
Contrary to the popular belief, there indeed is no God.