1. 3

    What’s the reason for the recent TLA flood on this site?

    Is this the new “hot” thing?

    1. 4

      I suspect it’s because there is more intro-level material for learning it now:

      Before then the most accessible resource that I’m aware of was the TLA+ Hyperbook. Reading a book is somehow more of a commitment, so fewer people bothered to learn.

    1. 10

      I know this post will sound really bad no matter how I say it, but I wonder how much of sexism, in the present (unlikely) or future (more likely) will be more fear than misogyny.

      Womens are becoming a touchy subjects and, in today’s world where a trial is decided by the public before it goes to court, a false rape accusation does more damage than the trial itself (at least imo). If I were an employer I’d be worried of female employees, not out of hatred or anything, but because they would hold so much power to screw me over.

      I personally don’t care what gender you are or religion or species.. I even like talking to assholes as long as they have something interesting to say. (Sadly I tend to be a bit of an asshole myself) But I would still be scared of talking to random women in a context like a conference because I might say something that puts me in a really bad place. It feels like I would be talking to someone with a loaded gun in my face.

      I think the best friends I have are those who made me notice my mistakes instead of assuming the worst of me, while the tech scene today seems more like a witch-hunting marathon to me.

      On that subject, why does the world have to work with cues and aggressive stances? Why can’t we be honest with each other? I see it every day, someone above me expects everyone to catch on her cues, if they don’t, they’re the bad guys, without even letting the other end knowing anything.

      Most angry tweets and blog posts about this topic are from people who just kept everything in or bursted out in anger at them and they got defensive or responded just as aggressively (kinda to be expected, honestly). I would love to see examples of people who were made aware of their behavior and everything went fine after that.

      1. 18

        a false rape accusation does more damage than the trial itself (at least imo).

        A genuine rape accusation also does more damage than the trial itself. In both cases, the victim is affected. It’s only how we perceive it that’s different.

        I think somewhere along the line communities started to encourage angry reactions as a way of maximising engagement. Somewhere along the line, we forgot to be kind by default, in a way we weren’t offline. I meet people who spend a lot of time in online communities, and you can see (amongst some people) that their online behaviour leaks into their personal offline behaviour, but rarely the other way.

        I think the recent furore over Equifax’s CSO having a music degree is a good example of this. Nobody should care about someone’s degree, but a marketwatch piece designed to provoke angry responses, provoked angry responses on the Internet. The Twitter algorithms designed to increase engagement increased engagement and the Internet went twitter crazy.

        There has to be a way to use a combo of the tools we use for engagement to promote de-escalation and de-engagement. Deprioritising inflammatory content to make the world a better place is not losing out. It’s winning.

        That’s what I really love about lobsters. People may have issues misinterpreting context and social cues here, but generally people are kind to each other.

        1. 10

          a false rape accusation does more damage than the trial itself

          That sort of accusation could, for example, prevent you from winning an Oscar. Or become elected US President.

          1. 11

            [Note: Before reading this, readers should probably know I have PTSD from a head injury. The side effects of nervous eyes, mumbly voice, and shaky hands apparently make me look like an easy target for male and female predators alike. I’m like a magnet for assholes who I usually deal with patiently, dismiss, or stand ground. Mostly ignore them. This issue required special treatment, though, since I was always treated very differently when it as something like this.]

            Far as scenario you’re worried about, it’s a real thing that’s happened to me multiple times. Not rape claims fortunately but sexual harassment or discrimination. I think I was getting false claims to managers two or three times a year with dozens making them to me directly as a warning or rebuke but not to my bosses. They just wanted me to worry that they could or would destroy me. Aside from the random ones, it was usually women who wanted a discount on something, wanted to be served ahead of other customers, or (with employees) not wanting to do the task they were given since it was beneath them or “man’s work.” Saying no to any of that was all it took…

            However, I was in a service position dealing with thousands of people plus dozens of workers due to high turnover. With all those people, just a few claims a year plus dozens of threats shows how rare this specific kind of bully is. Those that will fully push a false, gender-oriented claim are rare but highly damaging: each claim led people [that didn’t know me well] to assume I was guilty by default since I was male, interrogations by multiple supervisors or managers, and a waiting period for final results where I wondered if I’d loose my job and house with no work reference. Employment gaps on resumes make it harder to get new jobs in the U.S.. I got through those thanks to what I think were coworker’s testimony (mostly women) and managers’ judgment that the good and bad of me they’ve seen versus straight-up evil stuff a tiny number of women were claiming didn’t match up.

            Quick example: As a team supervisor, I always gave jobs to people in a semi-random way to try to be equal in what people had to do. Some supervisors seemed to cave in if a worker claimed the work was better for another gender, esp labor vs clerical vs people-focused work. When giving an assignment, the most shocking reply I got was from a beautiful, racially-mixed woman who had been a model and so on. A typically-good, funny worker who had a big ego. She said the specific task was a man’s job. I told her “I enforce equality like in the 19th Amendment here: women get equal rights, equal responsibilities.” She gave me a snobby look then said “I didn’t ask for that Amendment. Keep it, get rid of it, I don’t care. (Smirked and gestured about her appearance) I don’t need it. And I’m not doing man’s work.” I was a little stunned but kept insisting. She grudgingly did the job but poorly on purpose to disrupt our workflow. I had to correct that bias in my head where I assumed no woman would ever counter law’s or policies giving them equality outside maybe the religious. I was wrong…

            Back to false claims. That they defaulted against males, including other men who got hit with this, maybe for image reasons or just gender bias led me to change my behavior. Like I do in INFOSEC, I systematically looked for all the types of false claims people made esp what gave them believability. I then came up with mitigations even down to how I walk past attractive women on camera or go around them if off-camera. The specific words to use or avoid is important, esp consistency. I was pretty paranoid but supporting a house of five people when lots of layoffs were happening. The methods worked with a huge drop in threats and claims. Maybe the bullies had less superficial actions to use as leverage. So, I kept at it.

            This problem is one reason I work on teams with at least two people who are minorities that won’t lie for me. The latter ensures their credibility as witnesses. Main reason I like mixed teams is I like meeting and learning from new kinds of people. :) It’s a nice side benefit, though, that false claims dropped or ceased entirely when I’m on them for whatever reason. I’m still not sure given I don’t have enough data on that one. I also push for no-nonsense women, especially older with plenty of experience, to get management roles (a) since I’ve always promoted women in the workplace on principle and because mixed teams are more interesting; (b) side benefit that a woman whose dealt with and countered bullshit for years will be more likely to dismiss a false claim by a woman. When I finally got a female boss, esp who fought sexism to get there, the false claims that took serious investigation were handled usually in minutes by her. There was just one problem while she was there with a Hispanic woman… highly attractive with excellent ability to work crowds… that wanted my position launching a smear campaign. It almost worked but she had previously tried something on same manager she needed to convince. Her ego was so strong she didn’t think it would matter because she’d win her over too. Unbelievable lol. She left in a few months.

            So, yeah, I’d not go to one of these conferences at all probably. If I do, I’m bringing at least two women, one non-white, who barely like me but support the cause. If they leave me, I’m either going outside or doing something on my computer/phone against a wall or something. I’m not going to be in there alone at all given this specific type of bully or claim will likely win by default in such a place. Normally, though, I don’t mind being alone with women if there’s witnesses around that’s a mixed crowd, I’ve gotten to know them (trust them), or they’re one of the personalities that never pull stuff like this. I’ve gotten good at spotting those thanks to the jobs I did working with strangers all day. I get to relax more than you’d think from this comment, though, since vast majority of females on my team, other teams, and customers’ like me or at least neutral. The risk reducing behaviors are so habitual after years of doing them I barely notice I’m doing them until I see a post like this.

            Not funny note: There was also real sexism and harassment against women, esp from younger crowd. We had to deal with that, too. On rare events, some physical assault and stalkers that required police and other actions to deal with. One of the problems in many organizations is people will say the woman is making it up. Then, justice won’t happen. Our women were honest enough and male assholes brazen enough that we usually knew who was lying. Similarly when the women were bullshitting about harassment. In many other places or in trials, the defense was the woman might have been making it all up to spite the male. The reason that defense often works is because of the kind of bullies and lies I describe above. I get so pissed about false claims not just since they impacted me but because a steady stream of them in the media is used to prevent justice for real victims. That combination is why I write longer and fight harder on this issue.

            1. 9

              a false rape accusation does more damage than the trial itself (at least imo)

              In our society, a woman reporting a rape has to deal with a lot of shit from a lot of different people. Stuff like victim blaming, “What did you wear?”, “Oh you must’ve been reckless” make it already very hard for women to report rape when it happens. If anything we should be more concerned with women not reporting rape cases rather than false reports – especially since the latter is very small compared to the former. Sorry for not providing any sources, I’m on mobile right now.

              1. 15

                I know this post will sound really bad no matter how I say it,

                It does sound really bad. My favorite part is when you use the phrase “witch hunting” to somehow excuse the fear of women being around.

                but I wonder how much of sexism, in the present (unlikely) or future (more likely) will be more fear than misogyny.

                Oh so very little. Do not fear for mysoginy, it will be around forever.

                1. 16

                  My favorite part is when you use the phrase “witch hunting” to somehow excuse the fear of women being around.

                  I could not find a gender-neutral term that carried a similar meaning. This is definitely a fault on my part (my english dictionary is not that rich) but I was referring to the act of persecution by one or more individuals to the intended result of ruining someone’s life, humiliating them etc.

                  Oh so very little. Do not fear for mysoginy, it will be around forever.

                  What little hope for humanity and its self-improvement you seem to have. I understand the feeling.

                  My point was not whether misogyny will go away (it won’t), but how much of the perceived misogyny will be out of outright hatred rather than fear of consequences. Someone who doesn’t interact with women will be perceived as misogynous, but maybe he might just want to stay safe from ending up in a really bad situation? My “gun pointed at your head” analogy still stands. It feels uncomfortable and you can’t expect people to behave normally in those situations.

                  You seem to be the exact type of person I’m talking about, all going on the aggressive thinking I’m your worst enemy, not giving me the benefit of the doubt. I personally find it really hard to express my thoughts (it’s not just a language barrier, sadly), and getting attacked like that makes me really demoralized and demotivated to even talk. When I am not allowed to talk my mind without people instantly getting so aggressive at me, how am I supposed to not fear doing it?

                  1. 15

                    I personally find it really hard to express my thoughts (it’s not just a language barrier, sadly), and getting attacked like that makes me really demoralized and demotivated to even talk. When I am not allowed to talk my mind without people instantly getting so aggressive at me, how am I supposed to not fear doing it?

                    Thanks for saying this.

                    1. 5

                      I’m sorry that I sounded aggressive, because I was not trying to. I’m still not angry, nor replying out of spite or hate. :) I’m not a native english speaker (either?), so it can be that. Oh, and I also never thought of you as my worst enemy.

                      I could probably hug your right now, seriously, although I’m a little unsure how to understand your analogy that interacting with women is like having a gun pointed at your head.

                      As far as I can tell, we agree that misogyny will not go away – try to destroy an idea… – but we kinda disagree about how we should deal with it. I am not in a position to lecture anyone on the topic, and deeply nested threads tend to go off-topic easily, so I’ll happily reply to your emails if you’d like to.

                      1. 2

                        Thank you for your kind words, I’m sorry I misinterpreted your reply then!

                        I hate to link to it but I think that what best describes my analogy is a scenario like what ESR described. With no proof (even though the source claimed there had been attempts already) either back then or now, that was ruled as “unlikely” at best, but the fact that it doesn’t sound completely ridiculous and could be actually be put to action by a malicious group worries me.

                        I honestly don’t think most women are like that at all, and as you said, this is going a bit off topic.

                        About “how to deal with it”, I’m not proposing a solution, I do wonder if being more straightforward with people and less “I’ll totally blogpost this unacceptable behavior” would make anything easier though.

                        For example, the author quotes Berry’s paragraph about not giving anything for granted, yet instantly assumes that assuming that females are less technical is a big drag for women in tech. What about a little understanding? With so many women in sales and PR positions, the guy might be just tired as hell of having to deal with marketers (although the CTO title should have spoken for itself.)

                        Not denying that some people are just sexist jerks, though.

                    2. 8

                      Both literal witch hunts and the more recent metaphorical sense were frequently directed at men. The notion that “witch” is female is an ahistorical modern one and simply not part of what the word means in the context of a “witch hunt”.

                      1. 0

                        …So? Are you reading that Internet comment in the 1700s when historical witch hunts were actually happening?

                        1. 3

                          The witches arrested during the Salem Witch Trials (in 1692-3, around 150 being arrested) and killed (24, 20 executed, 4 died in jail) weren’t all women. A cursory scan of the accused show plenty of male names (although it does seem to bias towards women).

                      2. [Comment removed by author]

                        1. 12

                          US Americans are usually not aware that witches were systematically persecuted and killed.

                          That’s not true. Basically everyone learns about the Salem Witch Trials either in high school or via movies and other pop culture references.

                          1. 10

                            “US American” here, 2 things you have wrong:

                            • Witches weren’t only women: http://www.strangehistory.net/2012/06/21/all-hail-the-male-witch/ (witch was the term for being accused of witchcraft, not a term for women accused of witchcraft which is at best a modern reinterpretation of history)
                            • And we most definitely do get told about the systematic persecution and killing of witches.

                            And one thing not often known by Americans of their own witchcraft shenanigans, of the 21 executed Salem witches, 8 were men. https://en.wikipedia.org/wiki/List_of_people_of_the_Salem_witch_trials#Convicted_and_executed

                            As to witches again being even predominately women, only in certain areas, in Iceland iirc it was as high as 92% of witches were men. If we’re going to get angry at the use of witch to refer to women, lets at least get facts straight about the historical context.

                            1. 8

                              Not to mention that the primary accusers in Salem were female. It certainly wasn’t just man against woman.

                              1. 1

                                I dated two. They were awesome. Too bad our family moved around a lot. One actually taught me a little about the religion: Wicca. It involved men and women who (my interpretation) were basically nature worshipers. They usually didn’t cause harm because they believed the good or evil they did “came back times three.” When being deliberate rather than spontaneous, they were moderate in actions due to their Law of Extremes saying taking anything to the extreme of left or right makes it identical. That’s incorrect in the general case but there was truth in it where extremists are usually a problem regardless of the topic.

                                So, they tended to be friendly, non-conformist people that didn’t cause trouble unless provoked where they would warn then fight if necessary. Much like the Satanists I met as their rules similarly require not harming people or animals except in self-defense. For animals, also allowed to kill for food. Only common denominator among them that might inspire the religious choices were they had a lot of outcasts and rebels. The witches I knew were usually intuitive, artistic types whereas the Satanists were often intellectual with mix of artists and non-artists. I don’t know if the artist mix is just my data sample but the intellectual part makes sense given the greatest sin for Satanists is ignorance. They’re expected to pursue knowledge and call bullshit.

                                By the data, I’d have not worried about witches or Satanists. The majority of religious persecutors and violent offenders are Christian. They also push faith in authority over reason. They’re the most dangerous in the U.S. if I had to go by religion. In reality, all this stuff varies area to area, family to family, and person to person. I accept all groups so long as they’re not causing harm. Live and let live.

                                1. 6

                                  While I’m admittedly not an expert, I suspect the witches of the early US have little to do with Wicca, which was first introduced to the public in 1954.

                                  1. 1

                                    Possibly true. In that case, my experiences with witches wouldnt apply to those. I also suspect there’s a lot of different belief systems and groups using the word witch. Its meaning probably varies by group.

                          2. -2

                            The post content here is a man relating his experience of seeing his cofounder get talked over and ignored because she is a woman, so you immediately comment about… how bothersome it is that a woman might one day accuse you of sexual assault?

                            What the actual fuck is wrong with you? You should be thoroughly ashamed of yourself. Delete your account.

                            1. 16

                              What the actual fuck is wrong with you? You should be thoroughly ashamed of yourself. Delete your account.

                              I generally avoid these topics like the plague, but this is the exact reason why. It’s absolutely appalling to me that anyone thinks this is a good response to any comment ever. If you are trying to persuade people or this person, then you have completely failed in backing up your comments with anything but insults. If you aren’t trying to persuade anyone, then you are just a troll who enjoys yelling at someone who is clearly (based on the other comments in this thread) is trying to genuinely learn. You took a teaching moment and made it a display of hatred.

                              1. -1

                                If you are trying to persuade people or this person, then you have completely failed in backing up your comments with anything but insults

                                This assertion is completely absurd. I’ve been this asshole, been told off and/or beaten up, and learned better. Violent complaint is precisely how signalling to people that their behavior is utterly abhorrent works in society.

                                1. 6

                                  How should I signal to you that your behavior here, in this thread, is utterly abhorrent? Should I threaten to beat you up? Tell you to delete your account? Scream aggressive obscenities at you?

                                  Whatever it is you think you need to hear to stop behaving this way, pretend that I said it.

                                  1. 3

                                    I’ve been this asshole, been told off and/or beaten up, and learned better.

                                    I’ll just say that I find this comment immensely more helpful than your previous comment. If you’d like to expound on how specifically you’ve “been this asshole” in the past, and what you’ve learned from the experience I’d wager that’s much more likely to convince Hamcha (and the rest of us) to change their mind and behavior.

                                2. 5

                                  I questioned the reason she was ignored and proposed a motivation for which people might fear dealing with women. I also questioned what would have happened if the guy would have put any effort in making the issue clear to the people he’s talking shit about other than vague clues before making accusations with circumstantial evidence.

                                  What is there to be ashamed of?

                                  1. 3

                                    Normal people can have conversions with members of the opposite or same gender without constantly panicking about rape allegations. Do you specifically avoid female waiters at restaurants or cashiers at supermarkets? Is this somehow different to taking to a woman in a nontechnical role? If not, why do you think it is reasonable to pretend a woman who codes is any different? Hell, how on earth can you pretend the possibility of rape allegations is a valid reason to pretend that a person does not exist while in a meeting with multiple participants?

                                    Your regurgitation of sexist crap is shameful. Your lack of thought about it is bewildering. Delete your account.

                                  2. 3

                                    Who taught you to shame people for their feelings and beliefs?

                                    1. 0

                                      Some beliefs are horrendously evil. Your freedom to believe harmful crap does not constitute immunity from being yelled at for spouting it in public.

                                1. 5

                                  Taking a poke at fuzzers, in particular afl.

                                  Surprisingly simple to use, surprisingly effective.

                                  Highly recommended.

                                  1. 3

                                    Fuzzers are great. Last week at work I wrote a dead simple fuzzer (<100 lines) and found a bug that, if released, would have slowed a component of our storage service to a crawl. It likely would have been caught in pre-release QA, but it’s nice to catch that sort of thing early.

                                  1. 3

                                    Finally getting around to doing a swing migration of a couple terabytes of data. It’s been living on an old NTFS drive, so I’m swinging it over to a new hard drive. I’ll reformat the NTFS drive and bring the data back over (I want the new drive for something else because it’s bigger).

                                    I’m running Arch Linux and was hoping I could format both the drives with ZFS, but it’s not supported with my current kernel :( EXT4 it is

                                    1. 2

                                      Which kernel are you running? The zfs-dkms package in AUR might suit your needs.

                                      1. 1

                                        Second: I use zfs-dkms-git, spl-dkms-git, spl-utils-git and zfs-utils-git on four kernels. The only caveat is that pacmanʼs DKMS trigger doesnʼt always try to build spl and zfs in the right order, so itʼs important to check that one doesnʼt need to do sudo dkms install zfs/0.7.0 -k 4.… by hand.

                                        1. 2

                                          I’ve been using the standard kernel that ships with Arch. At this time, it’s 4.11.7. I remember hearing about those DKMS packages (I think from the Arch wiki for ZFS?) so I may have to give that a shot

                                    1. 1

                                      Looks useful! A related project is Metacademy. I think (most of?) the content is CC BY-SA and GFDL, so you may even be able to integrate it with your search engine if you wanted to.

                                      1. 2

                                        I was actually inspired by Metacademy. I especially love their idea of knowledge dependencies and it s something we are also planning to implement. We want to show all the required knowledge needed to effectively learn any of the topics.

                                      1. 42

                                        In case anyone wants to cross-check, out of the 23 curl CVEs in 2016, at least 10 (1, 2, 3, 4, 5, 6, 7, 8, 9, 10) are due to C’s manual memory management or weak typing and would be impossible in a memory-safe, strongly-typed language. (Note that, while I like Rust and it seems to have been the motivator for this post, many modern languages meet this bar.) While “slightly more than half” as non-C-related vulnerabilities may technically be “most”, I’m not sure it’s fitting the spirit of the term.

                                        There are some very compelling advantages to C, certainly, which the author enumerates; in particular, its portability to nearly every platform in existence is a major weakness of Rust (and, to the best of my knowledge, any other competitor) at the moment. But it’s very important to note that nontrivial C code practically always contains serious vulnerabilities, and nothing we’ve tried (especially “code better”, the standard advice for avoiding C vulnerabilities) works to prevent them. We should be conscious that, by writing C, we are trading away security in favor of whatever benefits C provides at that moment.

                                        edit: It’s worth noticing and noting, as I failed to, that 2016 was an unusual year for curl vulns. /u/amaurea on Reddit helpfully counted and cataloged all the vulns on that page, and 2016 is an obvious outlier for raw count, strongly suggesting an audit or new static analysis tool or something. However, the proportion of C to not-C bugs is not wildly varied over the entire list, so the point stands.

                                        1. 9

                                          […] 2016 is an obvious outlier for raw count, strongly suggesting an audit or new static analysis tool or something.

                                          It was an audit.

                                          1. 5

                                            especially “code better”, the standard advice for avoiding C vulnerabilities

                                            If the curl codebase is as bad as its API then this is honestly a completely fair response.

                                            We had this code recently:

                                            int status;
                                            void * some_pointer;
                                            curl_easy_getinfo( curl, CURLINFO_RESPONSE_CODE, &status );
                                            

                                            which trashes some_pointer on 64bit Linux because curl_easy_getinfo( CURLINFO_RESPONSE_CODE ) takes a pointer to a long and not an int. The compiler would normally warn about that, but curl_easy_getinfo is a varargs function, which brings no benefits and means the compiler can’t check the types of its arguments. WTF seriously? Why would you do that??

                                            I also recall reading somewhere that curl is over 100k LOC, which is insane. If the HTTP spec actually requires the implementation to be that large (and it wouldn’t surprise me if it does), then you are free to, and absolutely should, just not implement all of it. If the spec is so unwieldy that nobody could possibly get it right, then why try? Implement a sensible subset and call it a day.

                                            If you know you’re not going to be using many HTTP features, it’s not hard to implement it yourself and treat anything that isn’t part of the tiny subset you chose as an error. For example, it’s only a few hundred lines to implement synchronous GET requests with non-multipart responses and timeouts, and that’s often good enough.

                                            1. 5

                                              I also recall reading somewhere that curl is over 100k LOC, which is insane. If the HTTP spec actually requires the implementation to be that large (and it wouldn’t surprise me if it does), then you are free to, and absolutely should, just not implement all of it.

                                              curl supports a lot more protocols than just http though.

                                              1. 3

                                                Indeed. From the man page.

                                                curl is a tool to transfer data from or to a server, using one of the supported protocols (DICT, FILE, FTP, FTPS, GOPHER, HTTP, HTTPS, IMAP, IMAPS, LDAP, LDAPS, POP3, POP3S, RTMP, RTSP, SCP, SFTP, SMB, SMBS, SMTP, SMTPS, TELNET and TFTP).

                                                1. 1

                                                  damn, that’s a juicy attack surface

                                              2. 3

                                                CURL is highly compatible with a lot of the strange behaviors that browsers do support and are usually outside of (or even prohibited by) the spec/standard. Just implementing the spec doesn’t quite make it useful to the world, when the world isn’t even spec compliant. Even if you write down the standard, the real standard is what all the other browsers do, not what a piece of paper says.

                                                Example: https://github.com/curl/curl/issues/791

                                                1. 1

                                                  But it is useful even if you only implement a tiny subset of HTTP, because most use cases involve sending trivial requests to sensible servers.

                                                  1. 3

                                                    The point is that cURL isn’t a project that supplies that subset, regardless of it being useful or not. cURL supplies a complete and comprehensive package that runs pretty much anywhere and supports pretty much any protocol you might need at some point (and some you might not need).

                                                    Nothing wrong in making a slimmed down works-most-of-the-time-and-will-be-enough-for-most-people project, it might be very useful indeed, but thats not the goal of the cURL project. There’s space for both.

                                                    1. 1

                                                      This is the way. Start small. I would assume that 90% of the use cases for curl is just some simple HTTP(S) queries and that can be implemented in any language quite quickly.

                                                      For example, D currently has curl in its standard library, which will probably be deprecated and removed. For simple HTTP(S) queries, there is requests, which is pure D except for the ssl and crypto stuff.

                                                2. 8

                                                  nothing we’ve tried works to prevent them

                                                  Formal verification actually works. seL4 exists.

                                                  1. 10

                                                    Verifying seL4 took a few years and it was roughly 10000 LoC. Curl has an order of magnitude more. 113316 as counted by sloccount on the Github repo right now. Verification is getting easier, but only very slowly.

                                                    There is no immediate commercial advantage since curl works fine. This leaves it to academia to get the ball rolling.

                                                    1. 4

                                                      Verifying seL4 took a few years and it was roughly 10000 LoC.

                                                      Formally verifying 15,000ish lines of Haskell-generated C in seL4 took ~200,000 lines of proof, actually, per this. Formally verifying all of curl would easily run into the millions of lines of proof – and you’d basically be rewritting it into C-writing Haskell to boot.

                                                    2. 3

                                                      seL4 has two versions, a Haskell version that’s used to verify model safety and a C version that’s just a translation of the Haskell version. It may actually be a bit of a counter-example to your claim (that formal verification on C works in practice).

                                                      1. 1

                                                        This is incorrect. seL4 project actually proved C version is equivalent to (technically, refines) Haskell version. And then they (semi-automatically) proved generated assembly is equivalent to (refines) C so that they don’t need to rely on C compiler correctness.

                                                    3. 2

                                                      Yes but a lot of these are only published and fixed because curl is so widely used—and scrutinized. For example number 2 on your list:

                                                      If a username is set directly via CURLOPTUSERNAME (or curl’s -u, –user option), this vulnerability can be triggered. The name has to be at least 512MB big in a 32bit system. Systems with 64 bit versions of the sizet type are not affected by this issue.

                                                      Literally this doesn’t matter.

                                                      Also, how would Rust prevent this? I’m pretty sure multiplication overflow happens in Rust too.

                                                      1. 14

                                                        Rust specifies that:

                                                        1. If overflow happens, it is a “program error,” but is well-defined as two’s compliment wrapping.
                                                        2. In debug builds, overflow must be checked for and panic.

                                                        In the future, if overflow checking is cheap enough, this gives us the ability to require it. Who knows when that’ll ever be :)

                                                        Also note that this means it might lead to a logic error, but not a memory safety error. Just by making it defined helps a lot.

                                                        1. 3

                                                          Is there a formal or semi-formal Rust specification anywhere?

                                                          1. 9

                                                            Not quite yet; or at least, it’s not all in one place. While all those universities are working on formalisms, we’re not working hard to get one in place, since it’d have to take that work into account, which would mean throwing stuff out and re-writing it that way, I’d imagine.

                                                            There is some work going on to make the reference (linking to nightly docs since some work has recently landed to split it up into manageable chunks) closer to a spec; there’s also been an RFC accepted that says before stabilization, we must have the reference up-to-date with the changes, but we have to backfill all the older ones. So currently, it’s always accurate but not complete.

                                                            This area is well-specified though, in RFC 560 https://github.com/rust-lang/rfcs/blob/master/text/0560-integer-overflow.md (one RFC I refer to so often I remember its number by heart)

                                                            1. 1

                                                              Thank ye

                                                          2. 2

                                                            That’s neat! Still, I find it hard to believe anything would have coverage of all multiplication errors in allocations, even if it were written in Rust. If anyone can show me a single Rust project that deliberately trips the debug panic for multiplication errors during allocation in its unit tests, I’ll be impressed. But I’ll bet the only way to really be robust against this class of error is to use something like OpenBSD’s reallocarray. That’s equally possible in C and Rust.

                                                            1. 3

                                                              I do have an few overflow tests in one of my projects, but not for that specifically: https://github.com/steveklabnik/semver-parser/blob/master/src/range.rs#L682

                                                              We have pretty decent fuzzer support, seems like that might be something it would be likely to find.

                                                              1. 2

                                                                I guess that depends on how often you run your fuzzer on 32 but systems long enough for it to accumulate gigabytes of input.

                                                                The example here triggers after half a gig, but many of this class of bug would need more.