The best articles by Ciro Santilli Updated +Created
These are the best articles ever authored by Ciro Santilli, most of them in the format of Stack Overflow answers.
Ciro posts update about new articles on his Twitter accounts.
A chronological list of all articles is also kept at: Section "Updates".
Some random generally less technical in-tree essays will be present at: Section "Essays by Ciro Santilli".
USA spying on its own allies Updated +Created
Being Brazilian, Ciro Santilli is particularly curious about the existence of a Brazilian-focused website one mentioned in the article, as well as in other democracies.
WTF the CIA was doing in Brazil in the early 2010s! Wasn't helping to install the Military dictatorship in Brazil enough!
Here are the democracies found so far, defining a democracy as a country with score 7.0 or more in the Democracy index 2010. In native language:In English, so more deniable:"Almost democracies":Ciro couldn't help but feel as if looking through the Eyes of Sauron himself!
It is worth noting that democracies represent just a small minority of the websites found. The Middle East, and Spanish language sites (presumably for Venezuela + war on drugs countries?) where the huge majority. But Americans have to understand that democracies have to work together and build mutual trust, and not spy on one another. Even some of the enlightened people from Hacker News seem to not grasp this point. The USA cannot single handedly maintain world order as it once could. Collaboration based on trust is the only way.
Snowden's 2013 revelations particularly shocked USA allies with the fact that they were being spied upon, and as of the 2020's, everybody knows this and has "stopped caring", and or moved to end-to-end encryption by default. This is beautifully illustrated in the Snowden when Snowden talks about his time in Japan working for Dell as an undercover NSA operative:
NSA wanted to impress the Japanese. Show them our reach. They loved the live video from drones. This is Pakistan right now [video shows CIA agents demonstrating drone footage to Japanese officials]. They were not as excited about that we wanted their help to spy on the Japanese population. They said it was against their laws.
We bugged the country anyway, of course.
And we did not stop there. Once we had their communications we continued with the physical infrastructure. We sneaked into small programs in their power grids, dams, hospitals. The idea was that if Japan one day was not our allies we could turn off the lights.
And it was not just Japan. We planted software in Mexico, Germany, Brazil, Austria.
China, I can understand. Or Russia or Iran. Venezuela, okay.
But Austria? [shows footage of cow on an idyllic Alpine mountain grazing field, suggesting that there is nothing in Austria to spy on]
Another noteworthy scene from that movie is Video "Aptitude test scene from the Snowden 2016 film", where a bunch of new CIA recruits are told that:
Each of you is going to build a covert communications network in your home city [i.e. their fictitious foreign target location written on each person's desk, not necessarily where they were actually born], you're going to deploy it, backup your site, destroy it, and restore it again.
Incoming links Updated +Created
By Ciro Santilli:
By others:
Facebook profile face dump Updated +Created
In 2016 Ciro made a script downloaded Facebook profile pictures.
This was possible at the time without any login by using a 2010 profile ID dump from originally announced at: blog.skullsecurity.org/2010/return-of-the-facebook-snatchers since profile picture access was not authenticated.
The profile ID dump was downloadable through a BitTorrent named fbdata.torrent of about 2.8GB, mostly compressed. Doing:
find . -type f | xargs sha256sum | sha256sum
on Ubuntu 20.04 gives:
2c9a739c9c5495e38ebab81fc67411b7c6562f139dcb8619901a3f01230efdd5
This dump widely reported e.g. on Hacker News at: news.ycombinator.com/item?id=1554558.
At some point however, Facebook finally started to require tokens to view public profile pictures, thus making such further collection impossible, e.g. as of 2021: developers.facebook.com/docs/graph-api/reference/v9.0/user/picture mentions:
Querying a User ID (UID) now requires an access token.
This is also mentioned e.g. at: stackoverflow.com/questions/11442442/get-user-profile-picture-by-id. This major privacy flaw was therefore finally addressed at some point, making it impossible to reproduce this project.
Ciro downloaded 10 thousand of those pictures, and did facial extraction with: stackoverflow.com/questions/13211745/detect-face-then-autocrop-pictures/37501314#37501314
He then created single a video by joining 10 thousand of those cropped faces which can be uploaded e.g. to YouTube. Ciro later decided it was better to make those videos private however, as sooner later he'd lose his account for it.
Companies like YouTube blocking this kind of content is the type of thing that makes companies take longer to fix such gaping privacy issues, and is a bit like security through obscurity. A video makes it clear to everyone that there is a privacy issue very effectively. But people prefer to hide and look away, and then 99% of people who know nothing about tech get their privacy busted by actual criminals/government spies and never learn about it.
But now that Facebook finally fixed it, it's fine, no need for the video anymore.
Reactions to cirosantilli.com Updated +Created
Deep psychological analyses:
The Math Genome Project Updated +Created
Appears to support multiple proof assistant backends including Lean, Hol and Coq.
A discussion on the Lean Zulip: leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20Math.20Genome.20Project/near/352639129. Lean people are not convinced about the model in general it seems however.
TODO not viewable without login?
Has conjectures feature.
Built by this dude John Mercer: www.linkedin.com/in/johnmercer/. He must be independently wealthy or something? What a hero.
Ciro Santilli asked: discord.com/channels/1096393420408360989/1096393420408360996/1137047842159079474
Does the website actually automatically check the formal proofs, or is this intended to be implemented at some point? And if yes, is it intended to allow proofs to depend on other proofs of the website (possibly by other people)
Owner:
Hi Ciro, yes we will be releasing in-browser proof assistant environments/checkers (e.g. Lean). Our goal is not to replace the underlying open-source repos (e.g. Mathlib) so the main dependency will be on the current repos; then when statement formalizations and proofs come in and are certified they can be PR'd to the respective repos. So we will be the source of truth for the informal latex code but only a stepping stone and orchestration layer on the way to the respective formal libraries.
So apparently there will be proof checking, but nodependencies between proofs, you still have to pull request everywhing back and face the pain.