Email Gateway (Sep 09 2022 at 18:32): Email Gateway (Sep 09 2022 at 18:32):From: "\"Zhang, Cynthia X. (GSFC-710.0)[BOOZ ALLEN HAMILTON]\"" <cl-isabelle-users@lists.cam.ac.uk>
Hello, my name is Cynthia Zhang and I am a Supply Chain Risk Management Analyst at NASA. NASA is currently conducting a supply chain assessment of Isabelle. As stated in Sections 208 and 514 of the Consolidated Appropriations Act, 2022, Public Law 117-103, enacted March 15, 2022, a required step of our process is to verify the Country of Origin (CoO) information for the product (i.e., the country where the products were developed, manufactured, and assembled.)
As Isabelle is open source, we understand that this inquiry is not directly applicable, as contributions may be made from individuals from around the world. In this case, NASA is interested in confirming the following information:
1. Is there an organization which sponsors/publishes the project, or a primary developer who audits the code for potential vulnerabilities, errors, or malicious code? Y/N
2. Does Isabelle have an overseeing organization or individual along these lines? Y/N
1. If so, please provide the name of the organization and country they are established in.
If the information above is unknown or cannot be provided, we request that you provide the country or list of countries where the majority of contributions originate from to satisfy Sections 208 and 514 of the Consolidated Appropriations Act, 2022, Public Law 117-103, enacted March 15, 2022.
Thank you,
Cynthia
Email Gateway (Sep 11 2022 at 19:23):From: Makarius <makarius@sketis.net>
Hello Cynthia,
as the long-term release manager of the Isabelle prover platform, I might be
in the slightly awkward position to say a few words about Isabelle as
"organisation sui generis". Some other people might add to that later on.
First of all, here is the missing link the Public Law 117-103 mentioned above:
https://www.congress.gov/117/bills/hr2471/BILLS-117hr2471enr.pdf with its
sections 208 and 514:
"""
SEC. 208. None of the funds made available under this title
shall be obligated or expended for any new or enhanced information
technology program having total estimated development costs in
excess of $100,000,000, unless the Deputy Attorney General and
the investment review board certify to the Committees on Appro-
priations of the House of Representatives and the Senate that
the information technology program has appropriate program
management controls and contractor oversight mechanisms in place,
and that the program is compatible with the enterprise architecture
of the Department of Justice.
"""
(I don't think that 208 is relevant here.)
"""
SEC. 514. (a) None of the funds appropriated or otherwise
made available under this Act may be used by the Departments
of Commerce and Justice, the National Aeronautics and Space
Administration, or the National Science Foundation to acquire a
high-impact or moderate-impact information system, as defined for
security categorization in the National Institute of Standards and
Technology’s (NIST) Federal Information Processing Standard
Publication 199, ‘‘Standards for Security Categorization of Federal
Information and Information Systems’’ unless the agency has—
(1) reviewed the supply chain risk for the information
systems against criteria developed by NIST and the Federal
Bureau of Investigation (FBI) to inform acquisition decisions
for high-impact and moderate-impact information systems
within the Federal Government;
(2) reviewed the supply chain risk from the presumptive
awardee against available and relevant threat information pro-
vided by the FBI and other appropriate agencies; and
(3) in consultation with the FBI or other appropriate Fed-
eral entity, conducted an assessment of any risk of cyber-
espionage or sabotage associated with the acquisition of such
system, including any risk associated with such system being
produced, manufactured, or assembled by one or more entities
identified by the United States Government as posing a cyber
threat, including but not limited to, those that may be owned,
directed, or subsidized by the People’s Republic of China, the
Islamic Republic of Iran, the Democratic People’s Republic of
Korea, or the Russian Federation.
(b) None of the funds appropriated or otherwise made available
under this Act may be used to acquire a high-impact or moderate-
impact information system reviewed and assessed under subsection
(a) unless the head of the assessing entity described in subsection
(a) has—(1) developed, in consultation with NIST, the FBI, and
supply chain risk management experts, a mitigation strategy
for any identified risks;
(2) determined, in consultation with NIST and the FBI,
that the acquisition of such system is in the national interest
of the United States; and
(3) reported that determination to the Committees on
Appropriations of the House of Representatives and the Senate
and the agency Inspector General.
"""
That is a lot of legal text, but the main message seems to be that products
from certain "rogue countries" should be avoided.
Isabelle is a research product grown out of a long-term collaboration between
Univ. Cambridge (UK) and TU Munich (Germany). Other contributors are mostly
from countries of western Europe, the former "Free West" speaking in terms of
the Cold War.
Culturally, Isabelle is in fact very European in the classic sense, not to say
very Bavarian. US users might be confused by that, or might actually like it,
recalling a good time at Beer festivals before new waves of Plague and War
have reached Europe recently.
So formally, you could probably just tick off these boring legal questions and
proceed thinking about a properly founded decision for one prover platform or
another.
For this more interesting concern, I recommend to start with talks by Tom
Hales in the past 5 years, mostly about HOL Light and Lean Prover, but also
some other proof assistants. Here is a copy of the slides from Big Proof 2018
in Edinburgh, UK: https://www.icms.org.uk/downloads/bigproof/Hales.pdf
Page 16 is particularly interesting, as it shows pictures of buildings to
represent important provers (for formalized mathematics): HOL Light, Mizar,
Coq, Isabelle, Metamath, Lean (this is version 3, not the quite different
version 4).
I find the imagery due to Hales very fitting, especially for Isabelle: You are
standing on a very high edifice, which appears to be an agglomerate of towers
stacked on top of each other. You only see the transition of one tower of
concrete into another tower of glass and steel. Below and above are surely
further towers that are not visible in the picture!
That illustrates an important Isabelle principle: It is hard to tell where it
starts and where it ends, and you always learn something new that you have
never seen before. E.g. people often start with Isabelle/HOL (the logic) and
the Isabelle/Isar proof language, and think "now I know it". Then they learn
about Isabelle/ML (the mathematical programming language for symbolic logic),
and think "now I really know it". Then they learn about Isabelle/Scala (the
physical system integration language), and think "now I really do know it". As
our culture is pretty much alive and thriving, this process of discovery will
continue for years to come.
Apart from fancy pictures, here is also a formal record of the build artifacts
that contribute to Isabelle2022-RC1 (the current release candidate for the
final release planned for 23-Oct-2022):
https://isabelle.sketis.net/website-Isabelle2022-RC1/dist/index.html
That is only the main Isabelle platform with all its contributing components;
it can be likened to a "Linux distribution for formal mathematics".
Furthermore, you need to add the "Archive of Formal Proofs" for Isabelle
applications that are "automagically" maintained by the people behind Isabelle
to follow the evolution of Isabelle: https://www.isa-afp.org (this is not Lean
where every major version of the system causes great trouble to the
application space).
In contrast to the rather bold pictures due Tom Hales, my own presentations
about Isabelle used to refer to the more modest story of "Blind monks
examining an elephant". Here is a nice painting by Hanabusa Itchō:
https://en.wikipedia.org/wiki/Blind_men_and_an_elephant#/media/File:Blind_monks_examining_an_elephant.jpg
So each Isabelle user manages to grasp some aspects of the system (the
"beast"), but nobody has full hold of it. They can still tame the beast, by
exchanging their own discoveries with other participants. (And then publish
results in the Archive of Formal Proofs.)
In retrospect, I consider this imagery too simplistic for Isabelle as a large
"environment" or "landscape". So here is another painting by Hanabusa Itchō:
http://darumapedia-persons.blogspot.com/2016/12/hanabusa-itcho.html --- it
shows the holy mountain Fuji-san in the back, with people living (and toiling)
near a river in the front.
Here is another Fuji-san scene by a different artist:
https://en.wikipedia.org/wiki/Thirty-six_Views_of_Mount_Fuji#/media/File:Great_Wave_off_Kanagawa2.jpg
--- it looks terrific, but I guess that some Isabelle/AFP contributors did
feel such distress as the people in the boat, when struggling with formal
proofs in Isabelle :-)
Apart from art, here is also some science:
https://dl.acm.org/doi/10.1007/s00165-019-00492-1 "From LCF to Isabelle/HOL"
published in 2019 in a journal by the ACM.
That is an US American publisher, so it surely won't appear on any black-list
published by the US Congress.
Makarius
Email Gateway (Sep 15 2022 at 12:07):From: Gerwin Klein <kleing@unsw.edu.au>
Dear Cynthia,
In addition to what Makarius already posted, I think the following might be relevant: TU Munich is the main host of the Isabelle repository, which means direct contributions to the Isabelle code base can only be made by people with an account at that institution. All other contributions are made via a person that has account access.
There is no formal process for e.g. vulnerability checking, but the existing very large automated testing infrastructure (which includes the entire Archive of Formal Proofs) as well as the existing developer culture achieve a code quality with respect to vulnerabilities, errors and malicious code that is far above an average open source project with e.g. a pull-request process on GitHub.
While there is no single individual or organisation that publishes Isabelle (but the collection of developers that Makarius mentioned, with TU Munich, the University of Cambridge, and Makarius himself probably being the largest contributors), given that the repository is hosted at TU Munich, listing TU Munich as the organisation might suffice for administrative purposes.
Cheers,
Gerwin
Last updated: Apr 26 2024 at 04:17 UTC
