Vulnerabilidades

Rocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed. Local Unset Universe Checking inside a module is expected to last only until the module ends, and the global flag is restored, but the universe graph keeps its own copy which is…

The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport. A fixpoint may apply a rewrite along an equality between types to its recursive argument, which the guard checker accepts because the inductive type is…

The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter…

Lean 4 VS Code Extension is a Visual Studio Code extension for the Lean 4 proof assistant. Projects that use @leanprover/unicode-input-component are vulnerable to an XSS exploit in 0.1.9 of the package and lower. The component re-inserted text in the input element back into the input element as unescaped HTML. The…

Improper Neutralization of Input During Web Page Generation ('Cross-site Scripting') vulnerability in jd7777 Daily Proverb daily-proverb allows Stored XSS.This issue affects Daily Proverb: from n/a through <= 2.0.3.

Multiple SQL injection vulnerabilities in caladmin.inc.php in Proverbs Web Calendar 1.1 and earlier allow remote attackers to execute arbitrary SQL commands via the (1) loginname (aka Username) and (2) loginpass (aka Password) parameters to caladmin.php.